:: WAYBEL_0 semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

definition
let L be RelStr ;
let X be Subset of L;
attr X is directed means :Def1: :: WAYBEL_0:def 1
for x, y being Element of L st x in X & y in X holds
ex z being Element of L st
( z in X & x <= z & y <= z );
attr X is filtered means :Def2: :: WAYBEL_0:def 2
for x, y being Element of L st x in X & y in X holds
ex z being Element of L st
( z in X & z <= x & z <= y );
end;

:: deftheorem Def1 defines directed WAYBEL_0:def 1 :
for L being RelStr
for X being Subset of L holds
( X is directed iff for x, y being Element of L st x in X & y in X holds
ex z being Element of L st
( z in X & x <= z & y <= z ) );

:: deftheorem Def2 defines filtered WAYBEL_0:def 2 :
for L being RelStr
for X being Subset of L holds
( X is filtered iff for x, y being Element of L st x in X & y in X holds
ex z being Element of L st
( z in X & z <= x & z <= y ) );

theorem Th1: :: WAYBEL_0:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty transitive RelStr
for X being Subset of L holds
( ( not X is empty & X is directed ) iff for Y being finite Subset of X ex x being Element of L st
( x in X & x is_>=_than Y ) )
proof end;

theorem Th2: :: WAYBEL_0:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty transitive RelStr
for X being Subset of L holds
( ( not X is empty & X is filtered ) iff for Y being finite Subset of X ex x being Element of L st
( x in X & x is_<=_than Y ) )
proof end;

registration
let L be RelStr ;
cluster {} L -> directed filtered ;
coherence
( {} L is directed & {} L is filtered )
proof end;
end;

registration
let L be RelStr ;
cluster directed filtered Element of bool the carrier of L;
existence
ex b1 being Subset of L st
( b1 is directed & b1 is filtered )
proof end;
end;

theorem Th3: :: WAYBEL_0:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L1, L2 being RelStr st RelStr(# the carrier of L1,the InternalRel of L1 #) = RelStr(# the carrier of L2,the InternalRel of L2 #) holds
for X1 being Subset of L1
for X2 being Subset of L2 st X1 = X2 & X1 is directed holds
X2 is directed
proof end;

theorem :: WAYBEL_0:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L1, L2 being RelStr st RelStr(# the carrier of L1,the InternalRel of L1 #) = RelStr(# the carrier of L2,the InternalRel of L2 #) holds
for X1 being Subset of L1
for X2 being Subset of L2 st X1 = X2 & X1 is filtered holds
X2 is filtered
proof end;

theorem Th5: :: WAYBEL_0:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty reflexive RelStr
for x being Element of L holds
( {x} is directed & {x} is filtered )
proof end;

registration
let L be non empty reflexive RelStr ;
cluster non empty finite directed filtered Element of bool the carrier of L;
existence
ex b1 being Subset of L st
( b1 is directed & b1 is filtered & not b1 is empty & b1 is finite )
proof end;
end;

registration
let L be with_suprema RelStr ;
cluster [#] L -> directed ;
coherence
[#] L is directed
proof end;
end;

registration
let L be non empty upper-bounded RelStr ;
cluster [#] L -> directed ;
coherence
[#] L is directed
proof end;
end;

registration
let L be with_infima RelStr ;
cluster [#] L -> filtered ;
coherence
[#] L is filtered
proof end;
end;

registration
let L be non empty lower-bounded RelStr ;
cluster [#] L -> filtered ;
coherence
[#] L is filtered
proof end;
end;

definition
let L be non empty RelStr ;
let S be SubRelStr of L;
attr S is filtered-infs-inheriting means :Def3: :: WAYBEL_0:def 3
for X being filtered Subset of S st X <> {} & ex_inf_of X,L holds
"/\" X,L in the carrier of S;
attr S is directed-sups-inheriting means :Def4: :: WAYBEL_0:def 4
for X being directed Subset of S st X <> {} & ex_sup_of X,L holds
"\/" X,L in the carrier of S;
end;

:: deftheorem Def3 defines filtered-infs-inheriting WAYBEL_0:def 3 :
for L being non empty RelStr
for S being SubRelStr of L holds
( S is filtered-infs-inheriting iff for X being filtered Subset of S st X <> {} & ex_inf_of X,L holds
"/\" X,L in the carrier of S );

:: deftheorem Def4 defines directed-sups-inheriting WAYBEL_0:def 4 :
for L being non empty RelStr
for S being SubRelStr of L holds
( S is directed-sups-inheriting iff for X being directed Subset of S st X <> {} & ex_sup_of X,L holds
"\/" X,L in the carrier of S );

registration
let L be non empty RelStr ;
cluster infs-inheriting -> filtered-infs-inheriting SubRelStr of L;
coherence
for b1 being SubRelStr of L st b1 is infs-inheriting holds
b1 is filtered-infs-inheriting
proof end;
cluster sups-inheriting -> directed-sups-inheriting SubRelStr of L;
coherence
for b1 being SubRelStr of L st b1 is sups-inheriting holds
b1 is directed-sups-inheriting
proof end;
end;

registration
let L be non empty RelStr ;
cluster non empty strict full infs-inheriting sups-inheriting filtered-infs-inheriting directed-sups-inheriting SubRelStr of L;
existence
ex b1 being SubRelStr of L st
( b1 is infs-inheriting & b1 is sups-inheriting & not b1 is empty & b1 is full & b1 is strict )
proof end;
end;

theorem :: WAYBEL_0:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty transitive RelStr
for S being non empty full filtered-infs-inheriting SubRelStr of L
for X being filtered Subset of S st X <> {} & ex_inf_of X,L holds
( ex_inf_of X,S & "/\" X,S = "/\" X,L )
proof end;

theorem :: WAYBEL_0:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty transitive RelStr
for S being non empty full directed-sups-inheriting SubRelStr of L
for X being directed Subset of S st X <> {} & ex_sup_of X,L holds
( ex_sup_of X,S & "\/" X,S = "\/" X,L )
proof end;

definition
let L1, L2 be non empty 1-sorted ;
let f be Function of L1,L2;
let x be Element of L1;
:: original: .
redefine func f . x -> Element of L2;
coherence
f . x is Element of L2
proof end;
end;

definition
let L1, L2 be RelStr ;
let f be Function of L1,L2;
attr f is antitone means :: WAYBEL_0:def 5
for x, y being Element of L1 st x <= y holds
for a, b being Element of L2 st a = f . x & b = f . y holds
a >= b;
end;

:: deftheorem defines antitone WAYBEL_0:def 5 :
for L1, L2 being RelStr
for f being Function of L1,L2 holds
( f is antitone iff for x, y being Element of L1 st x <= y holds
for a, b being Element of L2 st a = f . x & b = f . y holds
a >= b );

definition
let L be 1-sorted ;
attr c2 is strict;
struct NetStr of L -> RelStr ;
aggr NetStr(# carrier, InternalRel, mapping #) -> NetStr of L;
sel mapping c2 -> Function of the carrier of c2,the carrier of L;
end;

registration
let L be 1-sorted ;
let X be non empty set ;
let O be Relation of X;
let F be Function of X,the carrier of L;
cluster NetStr(# X,O,F #) -> non empty ;
coherence
not NetStr(# X,O,F #) is empty
proof end;
end;

definition
let N be RelStr ;
attr N is directed means :Def6: :: WAYBEL_0:def 6
[#] N is directed;
end;

:: deftheorem Def6 defines directed WAYBEL_0:def 6 :
for N being RelStr holds
( N is directed iff [#] N is directed );

registration
let L be 1-sorted ;
cluster non empty reflexive transitive antisymmetric strict directed NetStr of L;
existence
ex b1 being strict NetStr of L st
( not b1 is empty & b1 is reflexive & b1 is transitive & b1 is antisymmetric & b1 is directed )
proof end;
end;

definition
let L be 1-sorted ;
mode prenet of L is non empty directed NetStr of L;
end;

definition
let L be 1-sorted ;
mode net of L is transitive prenet of L;
end;

definition
let L be non empty 1-sorted ;
let N be non empty NetStr of L;
func netmap N,L -> Function of N,L equals :: WAYBEL_0:def 7
the mapping of N;
coherence
the mapping of N is Function of N,L
;
let i be Element of N;
func N . i -> Element of L equals :: WAYBEL_0:def 8
the mapping of N . i;
correctness
coherence
the mapping of N . i is Element of L
;
;
end;

:: deftheorem defines netmap WAYBEL_0:def 7 :
for L being non empty 1-sorted
for N being non empty NetStr of L holds netmap N,L = the mapping of N;

:: deftheorem defines . WAYBEL_0:def 8 :
for L being non empty 1-sorted
for N being non empty NetStr of L
for i being Element of N holds N . i = the mapping of N . i;

definition
let L be non empty RelStr ;
let N be non empty NetStr of L;
attr N is monotone means :: WAYBEL_0:def 9
netmap N,L is monotone;
attr N is antitone means :: WAYBEL_0:def 10
netmap N,L is antitone;
end;

:: deftheorem defines monotone WAYBEL_0:def 9 :
for L being non empty RelStr
for N being non empty NetStr of L holds
( N is monotone iff netmap N,L is monotone );

:: deftheorem defines antitone WAYBEL_0:def 10 :
for L being non empty RelStr
for N being non empty NetStr of L holds
( N is antitone iff netmap N,L is antitone );

definition
let L be non empty 1-sorted ;
let N be non empty NetStr of L;
let X be set ;
pred N is_eventually_in X means :Def11: :: WAYBEL_0:def 11
ex i being Element of N st
for j being Element of N st i <= j holds
N . j in X;
pred N is_often_in X means :: WAYBEL_0:def 12
for i being Element of N ex j being Element of N st
( i <= j & N . j in X );
end;

:: deftheorem Def11 defines is_eventually_in WAYBEL_0:def 11 :
for L being non empty 1-sorted
for N being non empty NetStr of L
for X being set holds
( N is_eventually_in X iff ex i being Element of N st
for j being Element of N st i <= j holds
N . j in X );

:: deftheorem defines is_often_in WAYBEL_0:def 12 :
for L being non empty 1-sorted
for N being non empty NetStr of L
for X being set holds
( N is_often_in X iff for i being Element of N ex j being Element of N st
( i <= j & N . j in X ) );

theorem :: WAYBEL_0:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty 1-sorted
for N being non empty NetStr of L
for X, Y being set st X c= Y holds
( ( N is_eventually_in X implies N is_eventually_in Y ) & ( N is_often_in X implies N is_often_in Y ) )
proof end;

theorem :: WAYBEL_0:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty 1-sorted
for N being non empty NetStr of L
for X being set holds
( N is_eventually_in X iff not N is_often_in the carrier of L \ X )
proof end;

theorem :: WAYBEL_0:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty 1-sorted
for N being non empty NetStr of L
for X being set holds
( N is_often_in X iff not N is_eventually_in the carrier of L \ X )
proof end;

scheme :: WAYBEL_0:sch 1
HoldsEventually{ F1() -> non empty RelStr , F2() -> non empty NetStr of F1(), P1[ set ] } :
( F2() is_eventually_in { (F2() . k) where k is Element of F2() : P1[F2() . k] } iff ex i being Element of F2() st
for j being Element of F2() st i <= j holds
P1[F2() . j] )
proof end;

definition
let L be non empty RelStr ;
let N be non empty NetStr of L;
attr N is eventually-directed means :Def13: :: WAYBEL_0:def 13
for i being Element of N holds N is_eventually_in { (N . j) where j is Element of N : N . i <= N . j } ;
attr N is eventually-filtered means :Def14: :: WAYBEL_0:def 14
for i being Element of N holds N is_eventually_in { (N . j) where j is Element of N : N . i >= N . j } ;
end;

:: deftheorem Def13 defines eventually-directed WAYBEL_0:def 13 :
for L being non empty RelStr
for N being non empty NetStr of L holds
( N is eventually-directed iff for i being Element of N holds N is_eventually_in { (N . j) where j is Element of N : N . i <= N . j } );

:: deftheorem Def14 defines eventually-filtered WAYBEL_0:def 14 :
for L being non empty RelStr
for N being non empty NetStr of L holds
( N is eventually-filtered iff for i being Element of N holds N is_eventually_in { (N . j) where j is Element of N : N . i >= N . j } );

theorem Th11: :: WAYBEL_0:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty RelStr
for N being non empty NetStr of L holds
( N is eventually-directed iff for i being Element of N ex j being Element of N st
for k being Element of N st j <= k holds
N . i <= N . k )
proof end;

theorem Th12: :: WAYBEL_0:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty RelStr
for N being non empty NetStr of L holds
( N is eventually-filtered iff for i being Element of N ex j being Element of N st
for k being Element of N st j <= k holds
N . i >= N . k )
proof end;

registration
let L be non empty RelStr ;
cluster monotone -> eventually-directed NetStr of L;
coherence
for b1 being prenet of L st b1 is monotone holds
b1 is eventually-directed
proof end;
cluster antitone -> eventually-filtered NetStr of L;
coherence
for b1 being prenet of L st b1 is antitone holds
b1 is eventually-filtered
proof end;
end;

registration
let L be non empty reflexive RelStr ;
cluster strict monotone antitone eventually-directed eventually-filtered NetStr of L;
existence
ex b1 being prenet of L st
( b1 is monotone & b1 is antitone & b1 is strict )
proof end;
end;

definition
let L be RelStr ;
let X be Subset of L;
func downarrow X -> Subset of L means :Def15: :: WAYBEL_0:def 15
for x being Element of L holds
( x in it iff ex y being Element of L st
( y >= x & y in X ) );
existence
ex b1 being Subset of L st
for x being Element of L holds
( x in b1 iff ex y being Element of L st
( y >= x & y in X ) )
proof end;
uniqueness
for b1, b2 being Subset of L st ( for x being Element of L holds
( x in b1 iff ex y being Element of L st
( y >= x & y in X ) ) ) & ( for x being Element of L holds
( x in b2 iff ex y being Element of L st
( y >= x & y in X ) ) ) holds
b1 = b2
proof end;
func uparrow X -> Subset of L means :Def16: :: WAYBEL_0:def 16
for x being Element of L holds
( x in it iff ex y being Element of L st
( y <= x & y in X ) );
existence
ex b1 being Subset of L st
for x being Element of L holds
( x in b1 iff ex y being Element of L st
( y <= x & y in X ) )
proof end;
correctness
uniqueness
for b1, b2 being Subset of L st ( for x being Element of L holds
( x in b1 iff ex y being Element of L st
( y <= x & y in X ) ) ) & ( for x being Element of L holds
( x in b2 iff ex y being Element of L st
( y <= x & y in X ) ) ) holds
b1 = b2
;
proof end;
end;

:: deftheorem Def15 defines downarrow WAYBEL_0:def 15 :
for L being RelStr
for X, b3 being Subset of L holds
( b3 = downarrow X iff for x being Element of L holds
( x in b3 iff ex y being Element of L st
( y >= x & y in X ) ) );

:: deftheorem Def16 defines uparrow WAYBEL_0:def 16 :
for L being RelStr
for X, b3 being Subset of L holds
( b3 = uparrow X iff for x being Element of L holds
( x in b3 iff ex y being Element of L st
( y <= x & y in X ) ) );

theorem Th13: :: WAYBEL_0:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L1, L2 being RelStr st RelStr(# the carrier of L1,the InternalRel of L1 #) = RelStr(# the carrier of L2,the InternalRel of L2 #) holds
for X being Subset of L1
for Y being Subset of L2 st X = Y holds
( downarrow X = downarrow Y & uparrow X = uparrow Y )
proof end;

theorem Th14: :: WAYBEL_0:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty RelStr
for X being Subset of L holds downarrow X = { x where x is Element of L : ex y being Element of L st
( x <= y & y in X )
}
proof end;

theorem Th15: :: WAYBEL_0:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty RelStr
for X being Subset of L holds uparrow X = { x where x is Element of L : ex y being Element of L st
( x >= y & y in X )
}
proof end;

registration
let L be non empty reflexive RelStr ;
let X be non empty Subset of L;
cluster downarrow X -> non empty ;
coherence
not downarrow X is empty
proof end;
cluster uparrow X -> non empty ;
coherence
not uparrow X is empty
proof end;
end;

theorem Th16: :: WAYBEL_0:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being reflexive RelStr
for X being Subset of L holds
( X c= downarrow X & X c= uparrow X )
proof end;

definition
let L be non empty RelStr ;
let x be Element of L;
func downarrow x -> Subset of L equals :: WAYBEL_0:def 17
downarrow {x};
correctness
coherence
downarrow {x} is Subset of L
;
;
func uparrow x -> Subset of L equals :: WAYBEL_0:def 18
uparrow {x};
correctness
coherence
uparrow {x} is Subset of L
;
;
end;

:: deftheorem defines downarrow WAYBEL_0:def 17 :
for L being non empty RelStr
for x being Element of L holds downarrow x = downarrow {x};

:: deftheorem defines uparrow WAYBEL_0:def 18 :
for L being non empty RelStr
for x being Element of L holds uparrow x = uparrow {x};

theorem Th17: :: WAYBEL_0:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty RelStr
for x, y being Element of L holds
( y in downarrow x iff y <= x )
proof end;

theorem Th18: :: WAYBEL_0:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty RelStr
for x, y being Element of L holds
( y in uparrow x iff x <= y )
proof end;

theorem :: WAYBEL_0:19  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty reflexive antisymmetric RelStr
for x, y being Element of L st downarrow x = downarrow y holds
x = y
proof end;

theorem :: WAYBEL_0:20  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty reflexive antisymmetric RelStr
for x, y being Element of L st uparrow x = uparrow y holds
x = y
proof end;

theorem Th21: :: WAYBEL_0:21  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty transitive RelStr
for x, y being Element of L st x <= y holds
downarrow x c= downarrow y
proof end;

theorem Th22: :: WAYBEL_0:22  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty transitive RelStr
for x, y being Element of L st x <= y holds
uparrow y c= uparrow x
proof end;

registration
let L be non empty reflexive RelStr ;
let x be Element of L;
cluster downarrow x -> non empty directed ;
coherence
( not downarrow x is empty & downarrow x is directed )
proof end;
cluster uparrow x -> non empty filtered ;
coherence
( not uparrow x is empty & uparrow x is filtered )
proof end;
end;

definition
let L be RelStr ;
let X be Subset of L;
attr X is lower means :Def19: :: WAYBEL_0:def 19
for x, y being Element of L st x in X & y <= x holds
y in X;
attr X is upper means :Def20: :: WAYBEL_0:def 20
for x, y being Element of L st x in X & x <= y holds
y in X;
end;

:: deftheorem Def19 defines lower WAYBEL_0:def 19 :
for L being RelStr
for X being Subset of L holds
( X is lower iff for x, y being Element of L st x in X & y <= x holds
y in X );

:: deftheorem Def20 defines upper WAYBEL_0:def 20 :
for L being RelStr
for X being Subset of L holds
( X is upper iff for x, y being Element of L st x in X & x <= y holds
y in X );

registration
let L be RelStr ;
cluster lower upper Element of bool the carrier of L;
existence
ex b1 being Subset of L st
( b1 is lower & b1 is upper )
proof end;
end;

theorem Th23: :: WAYBEL_0:23  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being RelStr
for X being Subset of L holds
( X is lower iff downarrow X c= X )
proof end;

theorem Th24: :: WAYBEL_0:24  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being RelStr
for X being Subset of L holds
( X is upper iff uparrow X c= X )
proof end;

theorem :: WAYBEL_0:25  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L1, L2 being RelStr st RelStr(# the carrier of L1,the InternalRel of L1 #) = RelStr(# the carrier of L2,the InternalRel of L2 #) holds
for X1 being Subset of L1
for X2 being Subset of L2 st X1 = X2 holds
( ( X1 is lower implies X2 is lower ) & ( X1 is upper implies X2 is upper ) )
proof end;

theorem :: WAYBEL_0:26  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being RelStr
for A being Subset-Family of L st ( for X being Subset of L st X in A holds
X is lower ) holds
union A is lower Subset of L
proof end;

theorem Th27: :: WAYBEL_0:27  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being RelStr
for X, Y being Subset of L st X is lower & Y is lower holds
( X /\ Y is lower & X \/ Y is lower )
proof end;

theorem :: WAYBEL_0:28  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being RelStr
for A being Subset-Family of L st ( for X being Subset of L st X in A holds
X is upper ) holds
union A is upper Subset of L
proof end;

theorem Th29: :: WAYBEL_0:29  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being RelStr
for X, Y being Subset of L st X is upper & Y is upper holds
( X /\ Y is upper & X \/ Y is upper )
proof end;

registration
let L be non empty transitive RelStr ;
let X be Subset of L;
cluster downarrow X -> lower ;
coherence
downarrow X is lower
proof end;
cluster uparrow X -> upper ;
coherence
uparrow X is upper
proof end;
end;

registration
let L be non empty transitive RelStr ;
let x be Element of L;
cluster downarrow x -> lower ;
coherence
downarrow x is lower
;
cluster uparrow x -> upper ;
coherence
uparrow x is upper
;
end;

registration
let L be non empty RelStr ;
cluster [#] L -> lower upper ;
coherence
( [#] L is lower & [#] L is upper )
proof end;
end;

registration
let L be non empty RelStr ;
cluster non empty lower upper Element of bool the carrier of L;
existence
ex b1 being Subset of L st
( not b1 is empty & b1 is lower & b1 is upper )
proof end;
end;

registration
let L be non empty reflexive transitive RelStr ;
cluster non empty directed lower Element of bool the carrier of L;
existence
ex b1 being Subset of L st
( not b1 is empty & b1 is lower & b1 is directed )
proof end;
cluster non empty filtered upper Element of bool the carrier of L;
existence
ex b1 being Subset of L st
( not b1 is empty & b1 is upper & b1 is filtered )
proof end;
end;

registration
let L be with_suprema with_infima Poset;
cluster non empty directed filtered lower upper Element of bool the carrier of L;
existence
ex b1 being Subset of L st
( not b1 is empty & b1 is directed & b1 is filtered & b1 is lower & b1 is upper )
proof end;
end;

theorem Th30: :: WAYBEL_0:30  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty reflexive transitive RelStr
for X being Subset of L holds
( X is directed iff downarrow X is directed )
proof end;

registration
let L be non empty reflexive transitive RelStr ;
let X be directed Subset of L;
cluster downarrow X -> directed lower ;
coherence
downarrow X is directed
by Th30;
end;

theorem Th31: :: WAYBEL_0:31  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty reflexive transitive RelStr
for X being Subset of L
for x being Element of L holds
( x is_>=_than X iff x is_>=_than downarrow X )
proof end;

theorem Th32: :: WAYBEL_0:32  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty reflexive transitive RelStr
for X being Subset of L holds
( ex_sup_of X,L iff ex_sup_of downarrow X,L )
proof end;

theorem Th33: :: WAYBEL_0:33  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty reflexive transitive RelStr
for X being Subset of L st ex_sup_of X,L holds
sup X = sup (downarrow X)
proof end;

theorem :: WAYBEL_0:34  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty Poset
for x being Element of L holds
( ex_sup_of downarrow x,L & sup (downarrow x) = x )
proof end;

theorem Th35: :: WAYBEL_0:35  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty reflexive transitive RelStr
for X being Subset of L holds
( X is filtered iff uparrow X is filtered )
proof end;

registration
let L be non empty reflexive transitive RelStr ;
let X be filtered Subset of L;
cluster uparrow X -> filtered upper ;
coherence
uparrow X is filtered
by Th35;
end;

theorem Th36: :: WAYBEL_0:36  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty reflexive transitive RelStr
for X being Subset of L
for x being Element of L holds
( x is_<=_than X iff x is_<=_than uparrow X )
proof end;

theorem Th37: :: WAYBEL_0:37  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty reflexive transitive RelStr
for X being Subset of L holds
( ex_inf_of X,L iff ex_inf_of uparrow X,L )
proof end;

theorem Th38: :: WAYBEL_0:38  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty reflexive transitive RelStr
for X being Subset of L st ex_inf_of X,L holds
inf X = inf (uparrow X)
proof end;

theorem :: WAYBEL_0:39  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty Poset
for x being Element of L holds
( ex_inf_of uparrow x,L & inf (uparrow x) = x )
proof end;

definition
let L be non empty reflexive transitive RelStr ;
mode Ideal of L is non empty directed lower Subset of L;
mode Filter of L is non empty filtered upper Subset of L;
end;

theorem Th40: :: WAYBEL_0:40  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being antisymmetric with_suprema RelStr
for X being lower Subset of L holds
( X is directed iff for x, y being Element of L st x in X & y in X holds
x "\/" y in X )
proof end;

theorem Th41: :: WAYBEL_0:41  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being antisymmetric with_infima RelStr
for X being upper Subset of L holds
( X is filtered iff for x, y being Element of L st x in X & y in X holds
x "/\" y in X )
proof end;

theorem Th42: :: WAYBEL_0:42  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being with_suprema Poset
for X being non empty lower Subset of L holds
( X is directed iff for Y being finite Subset of X st Y <> {} holds
"\/" Y,L in X )
proof end;

theorem Th43: :: WAYBEL_0:43  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being with_infima Poset
for X being non empty upper Subset of L holds
( X is filtered iff for Y being finite Subset of X st Y <> {} holds
"/\" Y,L in X )
proof end;

theorem :: WAYBEL_0:44  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty antisymmetric RelStr st ( L is with_suprema or L is with_infima ) holds
for X, Y being Subset of L st X is lower & X is directed & Y is lower & Y is directed holds
X /\ Y is directed
proof end;

theorem :: WAYBEL_0:45  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty antisymmetric RelStr st ( L is with_suprema or L is with_infima ) holds
for X, Y being Subset of L st X is upper & X is filtered & Y is upper & Y is filtered holds
X /\ Y is filtered
proof end;

theorem :: WAYBEL_0:46  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being RelStr
for A being Subset-Family of L st ( for X being Subset of L st X in A holds
X is directed ) & ( for X, Y being Subset of L st X in A & Y in A holds
ex Z being Subset of L st
( Z in A & X \/ Y c= Z ) ) holds
for X being Subset of L st X = union A holds
X is directed
proof end;

theorem :: WAYBEL_0:47  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being RelStr
for A being Subset-Family of L st ( for X being Subset of L st X in A holds
X is filtered ) & ( for X, Y being Subset of L st X in A & Y in A holds
ex Z being Subset of L st
( Z in A & X \/ Y c= Z ) ) holds
for X being Subset of L st X = union A holds
X is filtered
proof end;

definition
let L be non empty reflexive transitive RelStr ;
let I be Ideal of L;
attr I is principal means :: WAYBEL_0:def 21
ex x being Element of L st
( x in I & x is_>=_than I );
end;

:: deftheorem defines principal WAYBEL_0:def 21 :
for L being non empty reflexive transitive RelStr
for I being Ideal of L holds
( I is principal iff ex x being Element of L st
( x in I & x is_>=_than I ) );

definition
let L be non empty reflexive transitive RelStr ;
let F be Filter of L;
attr F is principal means :: WAYBEL_0:def 22
ex x being Element of L st
( x in F & x is_<=_than F );
end;

:: deftheorem defines principal WAYBEL_0:def 22 :
for L being non empty reflexive transitive RelStr
for F being Filter of L holds
( F is principal iff ex x being Element of L st
( x in F & x is_<=_than F ) );

theorem :: WAYBEL_0:48  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty reflexive transitive RelStr
for I being Ideal of L holds
( I is principal iff ex x being Element of L st I = downarrow x )
proof end;

theorem :: WAYBEL_0:49  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty reflexive transitive RelStr
for F being Filter of L holds
( F is principal iff ex x being Element of L st F = uparrow x )
proof end;

definition
let L be non empty reflexive transitive RelStr ;
func Ids L -> set equals :: WAYBEL_0:def 23
{ X where X is Ideal of L : verum } ;
correctness
coherence
{ X where X is Ideal of L : verum } is set
;
;
func Filt L -> set equals :: WAYBEL_0:def 24
{ X where X is Filter of L : verum } ;
correctness
coherence
{ X where X is Filter of L : verum } is set
;
;
end;

:: deftheorem defines Ids WAYBEL_0:def 23 :
for L being non empty reflexive transitive RelStr holds Ids L = { X where X is Ideal of L : verum } ;

:: deftheorem defines Filt WAYBEL_0:def 24 :
for L being non empty reflexive transitive RelStr holds Filt L = { X where X is Filter of L : verum } ;

definition
let L be non empty reflexive transitive RelStr ;
func Ids_0 L -> set equals :: WAYBEL_0:def 25
(Ids L) \/ {{} };
correctness
coherence
(Ids L) \/ {{} } is set
;
;
func Filt_0 L -> set equals :: WAYBEL_0:def 26
(Filt L) \/ {{} };
correctness
coherence
(Filt L) \/ {{} } is set
;
;
end;

:: deftheorem defines Ids_0 WAYBEL_0:def 25 :
for L being non empty reflexive transitive RelStr holds Ids_0 L = (Ids L) \/ {{} };

:: deftheorem defines Filt_0 WAYBEL_0:def 26 :
for L being non empty reflexive transitive RelStr holds Filt_0 L = (Filt L) \/ {{} };

definition
let L be non empty RelStr ;
let X be Subset of L;
set D = { ("\/" Y,L) where Y is finite Subset of X : ex_sup_of Y,L } ;
A1: { ("\/" Y,L) where Y is finite Subset of X : ex_sup_of Y,L } c= the carrier of L
proof end;
func finsups X -> Subset of L equals :: WAYBEL_0:def 27
{ ("\/" Y,L) where Y is finite Subset of X : ex_sup_of Y,L } ;
correctness
coherence
{ ("\/" Y,L) where Y is finite Subset of X : ex_sup_of Y,L } is Subset of L
;
by A1;
set D = { ("/\" Y,L) where Y is finite Subset of X : ex_inf_of Y,L } ;
A2: { ("/\" Y,L) where Y is finite Subset of X : ex_inf_of Y,L } c= the carrier of L
proof end;
func fininfs X -> Subset of L equals :: WAYBEL_0:def 28
{ ("/\" Y,L) where Y is finite Subset of X : ex_inf_of Y,L } ;
correctness
coherence
{ ("/\" Y,L) where Y is finite Subset of X : ex_inf_of Y,L } is Subset of L
;
by A2;
end;

:: deftheorem defines finsups WAYBEL_0:def 27 :
for L being non empty RelStr
for X being Subset of L holds finsups X = { ("\/" Y,L) where Y is finite Subset of X : ex_sup_of Y,L } ;

:: deftheorem defines fininfs WAYBEL_0:def 28 :
for L being non empty RelStr
for X being Subset of L holds fininfs X = { ("/\" Y,L) where Y is finite Subset of X : ex_inf_of Y,L } ;

registration
let L be non empty antisymmetric lower-bounded RelStr ;
let X be Subset of L;
cluster finsups X -> non empty ;
coherence
not finsups X is empty
proof end;
end;

registration
let L be non empty antisymmetric upper-bounded RelStr ;
let X be Subset of L;
cluster fininfs X -> non empty ;
coherence
not fininfs X is empty
proof end;
end;

registration
let L be non empty reflexive antisymmetric RelStr ;
let X be non empty Subset of L;
cluster finsups X -> non empty ;
coherence
not finsups X is empty
proof end;
cluster fininfs X -> non empty ;
coherence
not fininfs X is empty
proof end;
end;

theorem Th50: :: WAYBEL_0:50  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty reflexive antisymmetric RelStr
for X being Subset of L holds
( X c= finsups X & X c= fininfs X )
proof end;

theorem Th51: :: WAYBEL_0:51  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty transitive RelStr
for X, F being Subset of L st ( for Y being finite Subset of X st Y <> {} holds
ex_sup_of Y,L ) & ( for x being Element of L st x in F holds
ex Y being finite Subset of X st
( ex_sup_of Y,L & x = "\/" Y,L ) ) & ( for Y being finite Subset of X st Y <> {} holds
"\/" Y,L in F ) holds
F is directed
proof end;

registration
let L be with_suprema Poset;
let X be Subset of L;
cluster finsups X -> directed ;
coherence
finsups X is directed
proof end;
end;

theorem Th52: :: WAYBEL_0:52  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty reflexive transitive RelStr
for X, F being Subset of L st ( for Y being finite Subset of X st Y <> {} holds
ex_sup_of Y,L ) & ( for x being Element of L st x in F holds
ex Y being finite Subset of X st
( ex_sup_of Y,L & x = "\/" Y,L ) ) & ( for Y being finite Subset of X st Y <> {} holds
"\/" Y,L in F ) holds
for x being Element of L holds
( x is_>=_than X iff x is_>=_than F )
proof end;

theorem Th53: :: WAYBEL_0:53  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty reflexive transitive RelStr
for X, F being Subset of L st ( for Y being finite Subset of X st Y <> {} holds
ex_sup_of Y,L ) & ( for x being Element of L st x in F holds
ex Y being finite Subset of X st
( ex_sup_of Y,L & x = "\/" Y,L ) ) & ( for Y being finite Subset of X st Y <> {} holds
"\/" Y,L in F ) holds
( ex_sup_of X,L iff ex_sup_of F,L )
proof end;

theorem Th54: :: WAYBEL_0:54  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty reflexive transitive RelStr
for X, F being Subset of L st ( for Y being finite Subset of X st Y <> {} holds
ex_sup_of Y,L ) & ( for x being Element of L st x in F holds
ex Y being finite Subset of X st
( ex_sup_of Y,L & x = "\/" Y,L ) ) & ( for Y being finite Subset of X st Y <> {} holds
"\/" Y,L in F ) & ex_sup_of X,L holds
sup F = sup X
proof end;

theorem :: WAYBEL_0:55  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being with_suprema Poset
for X being Subset of L st ( ex_sup_of X,L or L is complete ) holds
sup X = sup (finsups X)
proof end;

theorem Th56: :: WAYBEL_0:56  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty transitive RelStr
for X, F being Subset of L st ( for Y being finite Subset of X st Y <> {} holds
ex_inf_of Y,L ) & ( for x being Element of L st x in F holds
ex Y being finite Subset of X st
( ex_inf_of Y,L & x = "/\" Y,L ) ) & ( for Y being finite Subset of X st Y <> {} holds
"/\" Y,L in F ) holds
F is filtered
proof end;

registration
let L be with_infima Poset;
let X be Subset of L;
cluster fininfs X -> filtered ;
coherence
fininfs X is filtered
proof end;
end;

theorem Th57: :: WAYBEL_0:57  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty reflexive transitive RelStr
for X, F being Subset of L st ( for Y being finite Subset of X st Y <> {} holds
ex_inf_of Y,L ) & ( for x being Element of L st x in F holds
ex Y being finite Subset of X st
( ex_inf_of Y,L & x = "/\" Y,L ) ) & ( for Y being finite Subset of X st Y <> {} holds
"/\" Y,L in F ) holds
for x being Element of L holds
( x is_<=_than X iff x is_<=_than F )
proof end;

theorem Th58: :: WAYBEL_0:58  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty reflexive transitive RelStr
for X, F being Subset of L st ( for Y being finite Subset of X st Y <> {} holds
ex_inf_of Y,L ) & ( for x being Element of L st x in F holds
ex Y being finite Subset of X st
( ex_inf_of Y,L & x = "/\" Y,L ) ) & ( for Y being finite Subset of X st Y <> {} holds
"/\" Y,L in F ) holds
( ex_inf_of X,L iff ex_inf_of F,L )
proof end;

theorem Th59: :: WAYBEL_0:59  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty reflexive transitive RelStr
for X, F being Subset of L st ( for Y being finite Subset of X st Y <> {} holds
ex_inf_of Y,L ) & ( for x being Element of L st x in F holds
ex Y being finite Subset of X st
( ex_inf_of Y,L & x = "/\" Y,L ) ) & ( for Y being finite Subset of X st Y <> {} holds
"/\" Y,L in F ) & ex_inf_of X,L holds
inf F = inf X
proof end;

theorem :: WAYBEL_0:60  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being with_infima Poset
for X being Subset of L st ( ex_inf_of X,L or L is complete ) holds
inf X = inf (fininfs X)
proof end;

theorem :: WAYBEL_0:61  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being with_suprema Poset
for X being Subset of L holds
( X c= downarrow (finsups X) & ( for I being Ideal of L st X c= I holds
downarrow (finsups X) c= I ) )
proof end;

theorem :: WAYBEL_0:62  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being with_infima Poset
for X being Subset of L holds
( X c= uparrow (fininfs X) & ( for F being Filter of L st X c= F holds
uparrow (fininfs X) c= F ) )
proof end;

definition
let L be non empty RelStr ;
attr L is connected means :Def29: :: WAYBEL_0:def 29
for x, y being Element of L holds
( x <= y or y <= x );
end;

:: deftheorem Def29 defines connected WAYBEL_0:def 29 :
for L being non empty RelStr holds
( L is connected iff for x, y being Element of L holds
( x <= y or y <= x ) );

registration
cluster non empty reflexive trivial -> non empty reflexive connected RelStr ;
coherence
for b1 being non empty reflexive RelStr st b1 is trivial holds
b1 is connected
proof end;
end;

registration
cluster non empty connected RelStr ;
existence
ex b1 being non empty Poset st b1 is connected
proof end;
end;

definition
mode Chain is non empty connected Poset;
end;

registration
let L be Chain;
cluster L ~ -> connected ;
coherence
L ~ is connected
proof end;
end;

definition
mode Semilattice is with_infima Poset;
mode sup-Semilattice is with_suprema Poset;
mode LATTICE is with_suprema with_infima Poset;
end;

theorem :: WAYBEL_0:63  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being Semilattice
for X being non empty upper Subset of L holds
( X is Filter of L iff subrelstr X is meet-inheriting )
proof end;

theorem :: WAYBEL_0:64  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being sup-Semilattice
for X being non empty lower Subset of L holds
( X is Ideal of L iff subrelstr X is join-inheriting )
proof end;

definition
let S, T be non empty RelStr ;
let f be Function of S,T;
let X be Subset of S;
pred f preserves_inf_of X means :Def30: :: WAYBEL_0:def 30
( ex_inf_of X,S implies ( ex_inf_of f .: X,T & inf (f .: X) = f . (inf X) ) );
pred f preserves_sup_of X means :Def31: :: WAYBEL_0:def 31
( ex_sup_of X,S implies ( ex_sup_of f .: X,T & sup (f .: X) = f . (sup X) ) );
end;

:: deftheorem Def30 defines preserves_inf_of WAYBEL_0:def 30 :
for S, T being non empty RelStr
for f being Function of S,T
for X being Subset of S holds
( f preserves_inf_of X iff ( ex_inf_of X,S implies ( ex_inf_of f .: X,T & inf (f .: X) = f . (inf X) ) ) );

:: deftheorem Def31 defines preserves_sup_of WAYBEL_0:def 31 :
for S, T being non empty RelStr
for f being Function of S,T
for X being Subset of S holds
( f preserves_sup_of X iff ( ex_sup_of X,S implies ( ex_sup_of f .: X,T & sup (f .: X) = f . (sup X) ) ) );

theorem :: WAYBEL_0:65  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S1, S2, T1, T2 being non empty RelStr st RelStr(# the carrier of S1,the InternalRel of S1 #) = RelStr(# the carrier of T1,the InternalRel of T1 #) & RelStr(# the carrier of S2,the InternalRel of S2 #) = RelStr(# the carrier of T2,the InternalRel of T2 #) holds
for f being Function of S1,S2
for g being Function of T1,T2 st f = g holds
for X being Subset of S1
for Y being Subset of T1 st X = Y holds
( ( f preserves_sup_of X implies g preserves_sup_of Y ) & ( f preserves_inf_of X implies g preserves_inf_of Y ) )
proof end;

definition
let L1, L2 be non empty RelStr ;
let f be Function of L1,L2;
attr f is infs-preserving means :: WAYBEL_0:def 32
for X being Subset of L1 holds f preserves_inf_of X;
attr f is sups-preserving means :: WAYBEL_0:def 33
for X being Subset of L1 holds f preserves_sup_of X;
attr f is meet-preserving means :: WAYBEL_0:def 34
for x, y being Element of L1 holds f preserves_inf_of {x,y};
attr f is join-preserving means :: WAYBEL_0:def 35
for x, y being Element of L1 holds f preserves_sup_of {x,y};
attr f is filtered-infs-preserving means :: WAYBEL_0:def 36
for X being Subset of L1 st not X is empty & X is filtered holds
f preserves_inf_of X;
attr f is directed-sups-preserving means :: WAYBEL_0:def 37
for X being Subset of L1 st not X is empty & X is directed holds
f preserves_sup_of X;
end;

:: deftheorem defines infs-preserving WAYBEL_0:def 32 :
for L1, L2 being non empty RelStr
for f being Function of L1,L2 holds
( f is infs-preserving iff for X being Subset of L1 holds f preserves_inf_of X );

:: deftheorem defines sups-preserving WAYBEL_0:def 33 :
for L1, L2 being non empty RelStr
for f being Function of L1,L2 holds
( f is sups-preserving iff for X being Subset of L1 holds f preserves_sup_of X );

:: deftheorem defines meet-preserving WAYBEL_0:def 34 :
for L1, L2 being non empty RelStr
for f being Function of L1,L2 holds
( f is meet-preserving iff for x, y being Element of L1 holds f preserves_inf_of {x,y} );

:: deftheorem defines join-preserving WAYBEL_0:def 35 :
for L1, L2 being non empty RelStr
for f being Function of L1,L2 holds
( f is join-preserving iff for x, y being Element of L1 holds f preserves_sup_of {x,y} );

:: deftheorem defines filtered-infs-preserving WAYBEL_0:def 36 :
for L1, L2 being non empty RelStr
for f being Function of L1,L2 holds
( f is filtered-infs-preserving iff for X being Subset of L1 st not X is empty & X is filtered holds
f preserves_inf_of X );

:: deftheorem defines directed-sups-preserving WAYBEL_0:def 37 :
for L1, L2 being non empty RelStr
for f being Function of L1,L2 holds
( f is directed-sups-preserving iff for X being Subset of L1 st not X is empty & X is directed holds
f preserves_sup_of X );

registration
let L1, L2 be non empty RelStr ;
cluster infs-preserving -> meet-preserving filtered-infs-preserving Relation of the carrier of L1,the carrier of L2;
coherence
for b1 being Function of L1,L2 st b1 is infs-preserving holds
( b1 is filtered-infs-preserving & b1 is meet-preserving )
proof end;
cluster sups-preserving -> join-preserving directed-sups-preserving Relation of the carrier of L1,the carrier of L2;
coherence
for b1 being Function of L1,L2 st b1 is sups-preserving holds
( b1 is directed-sups-preserving & b1 is join-preserving )
proof end;
end;

definition
let S, T be RelStr ;
let f be Function of S,T;
attr f is isomorphic means :Def38: :: WAYBEL_0:def 38
( f is one-to-one & f is monotone & ex g being Function of T,S st
( g = f " & g is monotone ) ) if ( not S is empty & not T is empty )
otherwise ( S is empty & T is empty );
correctness
consistency
verum
;
;
end;

:: deftheorem Def38 defines isomorphic WAYBEL_0:def 38 :
for S, T being RelStr
for f being Function of S,T holds
( ( not S is empty & not T is empty implies ( f is isomorphic iff ( f is one-to-one & f is monotone & ex g being Function of T,S st
( g = f " & g is monotone ) ) ) ) & ( ( S is empty or T is empty ) implies ( f is isomorphic iff ( S is empty & T is empty ) ) ) );

theorem Th66: :: WAYBEL_0:66  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S, T being non empty RelStr
for f being Function of S,T holds
( f is isomorphic iff ( f is one-to-one & rng f = the carrier of T & ( for x, y being Element of S holds
( x <= y iff f . x <= f . y ) ) ) )
proof end;

registration
let S, T be non empty RelStr ;
cluster isomorphic -> one-to-one monotone Relation of the carrier of S,the carrier of T;
coherence
for b1 being Function of S,T st b1 is isomorphic holds
( b1 is one-to-one & b1 is monotone )
by Def38;
end;

theorem :: WAYBEL_0:67  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S, T being non empty RelStr
for f being Function of S,T st f is isomorphic holds
( f " is Function of T,S & rng (f " ) = the carrier of S )
proof end;

theorem :: WAYBEL_0:68  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S, T being non empty RelStr
for f being Function of S,T st f is isomorphic holds
for g being Function of T,S st g = f " holds
g is isomorphic
proof end;

theorem Th69: :: WAYBEL_0:69  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S, T being non empty Poset
for f being Function of S,T st ( for X being Filter of S holds f preserves_inf_of X ) holds
f is monotone
proof end;

theorem :: WAYBEL_0:70  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S, T being non empty Poset
for f being Function of S,T st ( for X being Filter of S holds f preserves_inf_of X ) holds
f is filtered-infs-preserving
proof end;

theorem :: WAYBEL_0:71  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being Semilattice
for T being non empty Poset
for f being Function of S,T st ( for X being finite Subset of S holds f preserves_inf_of X ) & ( for X being non empty filtered Subset of S holds f preserves_inf_of X ) holds
f is infs-preserving
proof end;

theorem Th72: :: WAYBEL_0:72  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S, T being non empty Poset
for f being Function of S,T st ( for X being Ideal of S holds f preserves_sup_of X ) holds
f is monotone
proof end;

theorem :: WAYBEL_0:73  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S, T being non empty Poset
for f being Function of S,T st ( for X being Ideal of S holds f preserves_sup_of X ) holds
f is directed-sups-preserving
proof end;

theorem :: WAYBEL_0:74  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being sup-Semilattice
for T being non empty Poset
for f being Function of S,T st ( for X being finite Subset of S holds f preserves_sup_of X ) & ( for X being non empty directed Subset of S holds f preserves_sup_of X ) holds
f is sups-preserving
proof end;

definition
let L be non empty reflexive RelStr ;
attr L is up-complete means :Def39: :: WAYBEL_0:def 39
for X being non empty directed Subset of L ex x being Element of L st
( x is_>=_than X & ( for y being Element of L st y is_>=_than X holds
x <= y ) );
end;

:: deftheorem Def39 defines up-complete WAYBEL_0:def 39 :
for L being non empty reflexive RelStr holds
( L is up-complete iff for X being non empty directed Subset of L ex x being Element of L st
( x is_>=_than X & ( for y being Element of L st y is_>=_than X holds
x <= y ) ) );

registration
cluster reflexive with_suprema up-complete -> reflexive with_suprema upper-bounded RelStr ;
coherence
for b1 being reflexive with_suprema RelStr st b1 is up-complete holds
b1 is upper-bounded
proof end;
end;

theorem :: WAYBEL_0:75  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty reflexive antisymmetric RelStr holds
( L is up-complete iff for X being non empty directed Subset of L holds ex_sup_of X,L )
proof end;

definition
let L be non empty reflexive RelStr ;
attr L is /\-complete means :Def40: :: WAYBEL_0:def 40
for X being non empty Subset of L ex x being Element of L st
( x is_<=_than X & ( for y being Element of L st y is_<=_than X holds
x >= y ) );
end;

:: deftheorem Def40 defines /\-complete WAYBEL_0:def 40 :
for L being non empty reflexive RelStr holds
( L is /\-complete iff for X being non empty Subset of L ex x being Element of L st
( x is_<=_than X & ( for y being Element of L st y is_<=_than X holds
x >= y ) ) );

theorem Th76: :: WAYBEL_0:76  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty reflexive antisymmetric RelStr holds
( L is /\-complete iff for X being non empty Subset of L holds ex_inf_of X,L )
proof end;

registration
cluster non empty reflexive complete -> non empty reflexive up-complete /\-complete RelStr ;
coherence
for b1 being non empty reflexive RelStr st b1 is complete holds
( b1 is up-complete & b1 is /\-complete )
proof end;
cluster non empty reflexive /\-complete -> non empty reflexive lower-bounded RelStr ;
coherence
for b1 being non empty reflexive RelStr st b1 is /\-complete holds
b1 is lower-bounded
proof end;
cluster non empty with_suprema lower-bounded up-complete -> non empty complete RelStr ;
coherence
for b1 being non empty Poset st b1 is up-complete & b1 is with_suprema & b1 is lower-bounded holds
b1 is complete
proof end;
end;

registration
cluster non empty reflexive antisymmetric /\-complete -> non empty reflexive antisymmetric with_infima RelStr ;
coherence
for b1 being non empty reflexive antisymmetric RelStr st b1 is /\-complete holds
b1 is with_infima
proof end;
end;

registration
cluster non empty reflexive antisymmetric upper-bounded /\-complete -> non empty reflexive antisymmetric with_suprema upper-bounded RelStr ;
coherence
for b1 being non empty reflexive antisymmetric upper-bounded RelStr st b1 is /\-complete holds
b1 is with_suprema
proof end;
end;

registration
cluster strict complete lower-bounded up-complete /\-complete RelStr ;
existence
ex b1 being LATTICE st
( b1 is complete & b1 is strict )
proof end;
end;