:: YELLOW_0 semantic presentation begin scheme :: YELLOW_0:sch 1 RelStrEx{ F1() -> non empty set , P1[ set , set ] } : ex L being non empty strict RelStr st ( the carrier of L = F1() & ( for a, b being Element of L holds ( a <= b iff P1[a,b] ) ) ) proof consider R being Relation of F1() such that A1: for a, b being Element of F1() holds ( [a,b] in R iff P1[a,b] ) from RELSET_1:sch_2(); take L = RelStr(# F1(),R #); ::_thesis: ( the carrier of L = F1() & ( for a, b being Element of L holds ( a <= b iff P1[a,b] ) ) ) thus the carrier of L = F1() ; ::_thesis: for a, b being Element of L holds ( a <= b iff P1[a,b] ) let a, b be Element of L; ::_thesis: ( a <= b iff P1[a,b] ) ( a <= b iff [a,b] in R ) by ORDERS_2:def_5; hence ( a <= b iff P1[a,b] ) by A1; ::_thesis: verum end; definition let A be non empty RelStr ; redefine attr A is reflexive means :: YELLOW_0:def 1 for x being Element of A holds x <= x; compatibility ( A is reflexive iff for x being Element of A holds x <= x ) proof thus ( A is reflexive implies for x being Element of A holds x <= x ) by ORDERS_2:1; ::_thesis: ( ( for x being Element of A holds x <= x ) implies A is reflexive ) assume A1: for x being Element of A holds x <= x ; ::_thesis: A is reflexive let x be set ; :: according to RELAT_2:def_1,ORDERS_2:def_2 ::_thesis: ( not x in the carrier of A or [x,x] in the InternalRel of A ) assume x in the carrier of A ; ::_thesis: [x,x] in the InternalRel of A then reconsider x = x as Element of A ; x <= x by A1; hence [x,x] in the InternalRel of A by ORDERS_2:def_5; ::_thesis: verum end; end; :: deftheorem defines reflexive YELLOW_0:def_1_:_ for A being non empty RelStr holds ( A is reflexive iff for x being Element of A holds x <= x ); definition let A be RelStr ; redefine attr A is transitive means :: YELLOW_0:def 2 for x, y, z being Element of A st x <= y & y <= z holds x <= z; compatibility ( A is transitive iff for x, y, z being Element of A st x <= y & y <= z holds x <= z ) proof thus ( A is transitive implies for x, y, z being Element of A st x <= y & y <= z holds x <= z ) by ORDERS_2:3; ::_thesis: ( ( for x, y, z being Element of A st x <= y & y <= z holds x <= z ) implies A is transitive ) assume A1: for x, y, z being Element of A st x <= y & y <= z holds x <= z ; ::_thesis: A is transitive let x, y, z be set ; :: according to RELAT_2:def_8,ORDERS_2:def_3 ::_thesis: ( not x in the carrier of A or not y in the carrier of A or not z in the carrier of A or not [x,y] in the InternalRel of A or not [y,z] in the InternalRel of A or [x,z] in the InternalRel of A ) assume A2: ( x in the carrier of A & y in the carrier of A & z in the carrier of A ) ; ::_thesis: ( not [x,y] in the InternalRel of A or not [y,z] in the InternalRel of A or [x,z] in the InternalRel of A ) assume A3: ( [x,y] in the InternalRel of A & [y,z] in the InternalRel of A ) ; ::_thesis: [x,z] in the InternalRel of A reconsider x = x, y = y, z = z as Element of A by A2; ( x <= y & y <= z ) by A3, ORDERS_2:def_5; then x <= z by A1; hence [x,z] in the InternalRel of A by ORDERS_2:def_5; ::_thesis: verum end; redefine attr A is antisymmetric means :: YELLOW_0:def 3 for x, y being Element of A st x <= y & y <= x holds x = y; compatibility ( A is antisymmetric iff for x, y being Element of A st x <= y & y <= x holds x = y ) proof thus ( A is antisymmetric implies for x, y being Element of A st x <= y & y <= x holds x = y ) by ORDERS_2:2; ::_thesis: ( ( for x, y being Element of A st x <= y & y <= x holds x = y ) implies A is antisymmetric ) assume A4: for x, y being Element of A st x <= y & y <= x holds x = y ; ::_thesis: A is antisymmetric let x, y be set ; :: according to RELAT_2:def_4,ORDERS_2:def_4 ::_thesis: ( not x in the carrier of A or not y in the carrier of A or not [x,y] in the InternalRel of A or not [y,x] in the InternalRel of A or x = y ) assume A5: ( x in the carrier of A & y in the carrier of A ) ; ::_thesis: ( not [x,y] in the InternalRel of A or not [y,x] in the InternalRel of A or x = y ) assume A6: ( [x,y] in the InternalRel of A & [y,x] in the InternalRel of A ) ; ::_thesis: x = y reconsider x = x, y = y as Element of A by A5; ( x <= y & y <= x ) by A6, ORDERS_2:def_5; hence x = y by A4; ::_thesis: verum end; end; :: deftheorem defines transitive YELLOW_0:def_2_:_ for A being RelStr holds ( A is transitive iff for x, y, z being Element of A st x <= y & y <= z holds x <= z ); :: deftheorem defines antisymmetric YELLOW_0:def_3_:_ for A being RelStr holds ( A is antisymmetric iff for x, y being Element of A st x <= y & y <= x holds x = y ); registration cluster non empty complete -> non empty with_suprema with_infima for RelStr ; coherence for b1 being non empty RelStr st b1 is complete holds ( b1 is with_suprema & b1 is with_infima ) by LATTICE3:12; cluster1 -element reflexive -> 1 -element reflexive transitive antisymmetric complete for RelStr ; coherence for b1 being 1 -element reflexive RelStr holds ( b1 is complete & b1 is transitive & b1 is antisymmetric ) proof let L be 1 -element reflexive RelStr ; ::_thesis: ( L is complete & L is transitive & L is antisymmetric ) set x = the Element of L; A1: for x, y being Element of L holds x = y by STRUCT_0:def_10; thus L is complete ::_thesis: ( L is transitive & L is antisymmetric ) proof let X be set ; :: according to LATTICE3:def_12 ::_thesis: ex b1 being Element of the carrier of L st ( X is_<=_than b1 & ( for b2 being Element of the carrier of L holds ( not X is_<=_than b2 or b1 <= b2 ) ) ) take the Element of L ; ::_thesis: ( X is_<=_than the Element of L & ( for b1 being Element of the carrier of L holds ( not X is_<=_than b1 or the Element of L <= b1 ) ) ) thus for y being Element of L st y in X holds y <= the Element of L by A1; :: according to LATTICE3:def_9 ::_thesis: for b1 being Element of the carrier of L holds ( not X is_<=_than b1 or the Element of L <= b1 ) let y be Element of L; ::_thesis: ( not X is_<=_than y or the Element of L <= y ) y = the Element of L by A1; hence ( not X is_<=_than y or the Element of L <= y ) by ORDERS_2:1; ::_thesis: verum end; thus L is transitive ::_thesis: L is antisymmetric proof let x, y, z be Element of L; :: according to YELLOW_0:def_2 ::_thesis: ( x <= y & y <= z implies x <= z ) thus ( x <= y & y <= z implies x <= z ) by A1; ::_thesis: verum end; let x be Element of L; :: according to YELLOW_0:def_3 ::_thesis: for y being Element of L st x <= y & y <= x holds x = y thus for y being Element of L st x <= y & y <= x holds x = y by A1; ::_thesis: verum end; end; registration let x be set ; let R be Relation of {x}; cluster RelStr(# {x},R #) -> 1 -element ; coherence RelStr(# {x},R #) is 1 -element proof thus the carrier of RelStr(# {x},R #) is 1 -element ; :: according to STRUCT_0:def_19 ::_thesis: verum end; end; registration cluster1 -element strict reflexive for RelStr ; existence ex b1 being RelStr st ( b1 is strict & b1 is 1 -element & b1 is reflexive ) proof set O = the Order of {{}}; take RelStr(# {{}}, the Order of {{}} #) ; ::_thesis: ( RelStr(# {{}}, the Order of {{}} #) is strict & RelStr(# {{}}, the Order of {{}} #) is 1 -element & RelStr(# {{}}, the Order of {{}} #) is reflexive ) thus ( RelStr(# {{}}, the Order of {{}} #) is strict & RelStr(# {{}}, the Order of {{}} #) is 1 -element & RelStr(# {{}}, the Order of {{}} #) is reflexive ) ; ::_thesis: verum end; end; theorem Th1: :: YELLOW_0:1 for P1, P2 being RelStr st RelStr(# the carrier of P1, the InternalRel of P1 #) = RelStr(# the carrier of P2, the InternalRel of P2 #) holds for a1, b1 being Element of P1 for a2, b2 being Element of P2 st a1 = a2 & b1 = b2 holds ( ( a1 <= b1 implies a2 <= b2 ) & ( a1 < b1 implies a2 < b2 ) ) proof let P1, P2 be RelStr ; ::_thesis: ( RelStr(# the carrier of P1, the InternalRel of P1 #) = RelStr(# the carrier of P2, the InternalRel of P2 #) implies for a1, b1 being Element of P1 for a2, b2 being Element of P2 st a1 = a2 & b1 = b2 holds ( ( a1 <= b1 implies a2 <= b2 ) & ( a1 < b1 implies a2 < b2 ) ) ) assume A1: RelStr(# the carrier of P1, the InternalRel of P1 #) = RelStr(# the carrier of P2, the InternalRel of P2 #) ; ::_thesis: for a1, b1 being Element of P1 for a2, b2 being Element of P2 st a1 = a2 & b1 = b2 holds ( ( a1 <= b1 implies a2 <= b2 ) & ( a1 < b1 implies a2 < b2 ) ) let a1, b1 be Element of P1; ::_thesis: for a2, b2 being Element of P2 st a1 = a2 & b1 = b2 holds ( ( a1 <= b1 implies a2 <= b2 ) & ( a1 < b1 implies a2 < b2 ) ) let a2, b2 be Element of P2; ::_thesis: ( a1 = a2 & b1 = b2 implies ( ( a1 <= b1 implies a2 <= b2 ) & ( a1 < b1 implies a2 < b2 ) ) ) A2: ( a2 <= b2 iff [a2,b2] in the InternalRel of P2 ) by ORDERS_2:def_5; ( a1 <= b1 iff [a1,b1] in the InternalRel of P1 ) by ORDERS_2:def_5; hence ( a1 = a2 & b1 = b2 implies ( ( a1 <= b1 implies a2 <= b2 ) & ( a1 < b1 implies a2 < b2 ) ) ) by A1, A2, ORDERS_2:def_6; ::_thesis: verum end; theorem Th2: :: YELLOW_0:2 for P1, P2 being RelStr st RelStr(# the carrier of P1, the InternalRel of P1 #) = RelStr(# the carrier of P2, the InternalRel of P2 #) holds for X being set for a1 being Element of P1 for a2 being Element of P2 st a1 = a2 holds ( ( X is_<=_than a1 implies X is_<=_than a2 ) & ( X is_>=_than a1 implies X is_>=_than a2 ) ) proof let P1, P2 be RelStr ; ::_thesis: ( RelStr(# the carrier of P1, the InternalRel of P1 #) = RelStr(# the carrier of P2, the InternalRel of P2 #) implies for X being set for a1 being Element of P1 for a2 being Element of P2 st a1 = a2 holds ( ( X is_<=_than a1 implies X is_<=_than a2 ) & ( X is_>=_than a1 implies X is_>=_than a2 ) ) ) assume A1: RelStr(# the carrier of P1, the InternalRel of P1 #) = RelStr(# the carrier of P2, the InternalRel of P2 #) ; ::_thesis: for X being set for a1 being Element of P1 for a2 being Element of P2 st a1 = a2 holds ( ( X is_<=_than a1 implies X is_<=_than a2 ) & ( X is_>=_than a1 implies X is_>=_than a2 ) ) let X be set ; ::_thesis: for a1 being Element of P1 for a2 being Element of P2 st a1 = a2 holds ( ( X is_<=_than a1 implies X is_<=_than a2 ) & ( X is_>=_than a1 implies X is_>=_than a2 ) ) let a1 be Element of P1; ::_thesis: for a2 being Element of P2 st a1 = a2 holds ( ( X is_<=_than a1 implies X is_<=_than a2 ) & ( X is_>=_than a1 implies X is_>=_than a2 ) ) let a2 be Element of P2; ::_thesis: ( a1 = a2 implies ( ( X is_<=_than a1 implies X is_<=_than a2 ) & ( X is_>=_than a1 implies X is_>=_than a2 ) ) ) assume A2: a1 = a2 ; ::_thesis: ( ( X is_<=_than a1 implies X is_<=_than a2 ) & ( X is_>=_than a1 implies X is_>=_than a2 ) ) thus ( X is_<=_than a1 implies X is_<=_than a2 ) ::_thesis: ( X is_>=_than a1 implies X is_>=_than a2 ) proof assume A3: for b being Element of P1 st b in X holds b <= a1 ; :: according to LATTICE3:def_9 ::_thesis: X is_<=_than a2 let b2 be Element of P2; :: according to LATTICE3:def_9 ::_thesis: ( not b2 in X or b2 <= a2 ) assume b2 in X ; ::_thesis: b2 <= a2 hence b2 <= a2 by A1, A2, A3, Th1; ::_thesis: verum end; assume A4: for b being Element of P1 st b in X holds a1 <= b ; :: according to LATTICE3:def_8 ::_thesis: X is_>=_than a2 let b2 be Element of P2; :: according to LATTICE3:def_8 ::_thesis: ( not b2 in X or a2 <= b2 ) assume b2 in X ; ::_thesis: a2 <= b2 hence a2 <= b2 by A1, A2, A4, Th1; ::_thesis: verum end; theorem :: YELLOW_0:3 for P1, P2 being RelStr st RelStr(# the carrier of P1, the InternalRel of P1 #) = RelStr(# the carrier of P2, the InternalRel of P2 #) & P1 is complete holds P2 is complete proof let P1, P2 be RelStr ; ::_thesis: ( RelStr(# the carrier of P1, the InternalRel of P1 #) = RelStr(# the carrier of P2, the InternalRel of P2 #) & P1 is complete implies P2 is complete ) assume that A1: RelStr(# the carrier of P1, the InternalRel of P1 #) = RelStr(# the carrier of P2, the InternalRel of P2 #) and A2: for X being set ex a being Element of P1 st ( X is_<=_than a & ( for b being Element of P1 st X is_<=_than b holds a <= b ) ) ; :: according to LATTICE3:def_12 ::_thesis: P2 is complete let X be set ; :: according to LATTICE3:def_12 ::_thesis: ex b1 being Element of the carrier of P2 st ( X is_<=_than b1 & ( for b2 being Element of the carrier of P2 holds ( not X is_<=_than b2 or b1 <= b2 ) ) ) consider a being Element of P1 such that A3: X is_<=_than a and A4: for b being Element of P1 st X is_<=_than b holds a <= b by A2; reconsider a9 = a as Element of P2 by A1; take a9 ; ::_thesis: ( X is_<=_than a9 & ( for b1 being Element of the carrier of P2 holds ( not X is_<=_than b1 or a9 <= b1 ) ) ) thus X is_<=_than a9 by A1, A3, Th2; ::_thesis: for b1 being Element of the carrier of P2 holds ( not X is_<=_than b1 or a9 <= b1 ) let b9 be Element of P2; ::_thesis: ( not X is_<=_than b9 or a9 <= b9 ) reconsider b = b9 as Element of P1 by A1; assume X is_<=_than b9 ; ::_thesis: a9 <= b9 then a <= b by A1, A4, Th2; hence a9 <= b9 by A1, Th1; ::_thesis: verum end; theorem Th4: :: YELLOW_0:4 for L being transitive RelStr for x, y being Element of L st x <= y holds for X being set holds ( ( y is_<=_than X implies x is_<=_than X ) & ( x is_>=_than X implies y is_>=_than X ) ) proof let L be transitive RelStr ; ::_thesis: for x, y being Element of L st x <= y holds for X being set holds ( ( y is_<=_than X implies x is_<=_than X ) & ( x is_>=_than X implies y is_>=_than X ) ) let x, y be Element of L; ::_thesis: ( x <= y implies for X being set holds ( ( y is_<=_than X implies x is_<=_than X ) & ( x is_>=_than X implies y is_>=_than X ) ) ) assume A1: x <= y ; ::_thesis: for X being set holds ( ( y is_<=_than X implies x is_<=_than X ) & ( x is_>=_than X implies y is_>=_than X ) ) let X be set ; ::_thesis: ( ( y is_<=_than X implies x is_<=_than X ) & ( x is_>=_than X implies y is_>=_than X ) ) hereby ::_thesis: ( x is_>=_than X implies y is_>=_than X ) assume A2: y is_<=_than X ; ::_thesis: x is_<=_than X thus x is_<=_than X ::_thesis: verum proof let z be Element of L; :: according to LATTICE3:def_8 ::_thesis: ( not z in X or x <= z ) assume z in X ; ::_thesis: x <= z then z >= y by A2, LATTICE3:def_8; hence x <= z by A1, ORDERS_2:3; ::_thesis: verum end; end; assume A3: x is_>=_than X ; ::_thesis: y is_>=_than X let z be Element of L; :: according to LATTICE3:def_9 ::_thesis: ( not z in X or z <= y ) assume z in X ; ::_thesis: z <= y then x >= z by A3, LATTICE3:def_9; hence z <= y by A1, ORDERS_2:3; ::_thesis: verum end; theorem Th5: :: YELLOW_0:5 for L being non empty RelStr for X being set for x being Element of L holds ( ( x is_>=_than X implies x is_>=_than X /\ the carrier of L ) & ( x is_>=_than X /\ the carrier of L implies x is_>=_than X ) & ( x is_<=_than X implies x is_<=_than X /\ the carrier of L ) & ( x is_<=_than X /\ the carrier of L implies x is_<=_than X ) ) proof let L be non empty RelStr ; ::_thesis: for X being set for x being Element of L holds ( ( x is_>=_than X implies x is_>=_than X /\ the carrier of L ) & ( x is_>=_than X /\ the carrier of L implies x is_>=_than X ) & ( x is_<=_than X implies x is_<=_than X /\ the carrier of L ) & ( x is_<=_than X /\ the carrier of L implies x is_<=_than X ) ) let X be set ; ::_thesis: for x being Element of L holds ( ( x is_>=_than X implies x is_>=_than X /\ the carrier of L ) & ( x is_>=_than X /\ the carrier of L implies x is_>=_than X ) & ( x is_<=_than X implies x is_<=_than X /\ the carrier of L ) & ( x is_<=_than X /\ the carrier of L implies x is_<=_than X ) ) let x be Element of L; ::_thesis: ( ( x is_>=_than X implies x is_>=_than X /\ the carrier of L ) & ( x is_>=_than X /\ the carrier of L implies x is_>=_than X ) & ( x is_<=_than X implies x is_<=_than X /\ the carrier of L ) & ( x is_<=_than X /\ the carrier of L implies x is_<=_than X ) ) set Y = X /\ the carrier of L; thus ( X is_<=_than x implies X /\ the carrier of L is_<=_than x ) ::_thesis: ( ( x is_>=_than X /\ the carrier of L implies x is_>=_than X ) & ( x is_<=_than X implies x is_<=_than X /\ the carrier of L ) & ( x is_<=_than X /\ the carrier of L implies x is_<=_than X ) ) proof assume A1: for b being Element of L st b in X holds b <= x ; :: according to LATTICE3:def_9 ::_thesis: X /\ the carrier of L is_<=_than x let b be Element of L; :: according to LATTICE3:def_9 ::_thesis: ( not b in X /\ the carrier of L or b <= x ) assume b in X /\ the carrier of L ; ::_thesis: b <= x then b in X by XBOOLE_0:def_4; hence b <= x by A1; ::_thesis: verum end; thus ( X /\ the carrier of L is_<=_than x implies X is_<=_than x ) ::_thesis: ( x is_<=_than X iff x is_<=_than X /\ the carrier of L ) proof assume A2: for b being Element of L st b in X /\ the carrier of L holds b <= x ; :: according to LATTICE3:def_9 ::_thesis: X is_<=_than x let b be Element of L; :: according to LATTICE3:def_9 ::_thesis: ( not b in X or b <= x ) assume b in X ; ::_thesis: b <= x then b in X /\ the carrier of L by XBOOLE_0:def_4; hence b <= x by A2; ::_thesis: verum end; thus ( X is_>=_than x implies X /\ the carrier of L is_>=_than x ) ::_thesis: ( x is_<=_than X /\ the carrier of L implies x is_<=_than X ) proof assume A3: for b being Element of L st b in X holds b >= x ; :: according to LATTICE3:def_8 ::_thesis: X /\ the carrier of L is_>=_than x let b be Element of L; :: according to LATTICE3:def_8 ::_thesis: ( not b in X /\ the carrier of L or x <= b ) assume b in X /\ the carrier of L ; ::_thesis: x <= b then b in X by XBOOLE_0:def_4; hence x <= b by A3; ::_thesis: verum end; thus ( X /\ the carrier of L is_>=_than x implies X is_>=_than x ) ::_thesis: verum proof assume A4: for b being Element of L st b in X /\ the carrier of L holds b >= x ; :: according to LATTICE3:def_8 ::_thesis: X is_>=_than x let b be Element of L; :: according to LATTICE3:def_8 ::_thesis: ( not b in X or x <= b ) assume b in X ; ::_thesis: x <= b then b in X /\ the carrier of L by XBOOLE_0:def_4; hence x <= b by A4; ::_thesis: verum end; end; theorem Th6: :: YELLOW_0:6 for L being RelStr for a being Element of L holds ( {} is_<=_than a & {} is_>=_than a ) proof let L be RelStr ; ::_thesis: for a being Element of L holds ( {} is_<=_than a & {} is_>=_than a ) let a be Element of L; ::_thesis: ( {} is_<=_than a & {} is_>=_than a ) thus {} is_<=_than a ::_thesis: {} is_>=_than a proof let b be Element of L; :: according to LATTICE3:def_9 ::_thesis: ( not b in {} or b <= a ) thus ( not b in {} or b <= a ) ; ::_thesis: verum end; let b be Element of L; :: according to LATTICE3:def_8 ::_thesis: ( not b in {} or a <= b ) thus ( not b in {} or a <= b ) ; ::_thesis: verum end; theorem Th7: :: YELLOW_0:7 for L being RelStr for a, b being Element of L holds ( ( a is_<=_than {b} implies a <= b ) & ( a <= b implies a is_<=_than {b} ) & ( a is_>=_than {b} implies b <= a ) & ( b <= a implies a is_>=_than {b} ) ) proof let L be RelStr ; ::_thesis: for a, b being Element of L holds ( ( a is_<=_than {b} implies a <= b ) & ( a <= b implies a is_<=_than {b} ) & ( a is_>=_than {b} implies b <= a ) & ( b <= a implies a is_>=_than {b} ) ) let a, b be Element of L; ::_thesis: ( ( a is_<=_than {b} implies a <= b ) & ( a <= b implies a is_<=_than {b} ) & ( a is_>=_than {b} implies b <= a ) & ( b <= a implies a is_>=_than {b} ) ) A1: b in {b} by TARSKI:def_1; hence ( a is_<=_than {b} implies a <= b ) by LATTICE3:def_8; ::_thesis: ( ( a <= b implies a is_<=_than {b} ) & ( a is_>=_than {b} implies b <= a ) & ( b <= a implies a is_>=_than {b} ) ) hereby ::_thesis: ( a is_>=_than {b} iff b <= a ) assume A2: a <= b ; ::_thesis: a is_<=_than {b} thus a is_<=_than {b} ::_thesis: verum proof let c be Element of L; :: according to LATTICE3:def_8 ::_thesis: ( not c in {b} or a <= c ) thus ( not c in {b} or a <= c ) by A2, TARSKI:def_1; ::_thesis: verum end; end; thus ( a is_>=_than {b} implies a >= b ) by A1, LATTICE3:def_9; ::_thesis: ( b <= a implies a is_>=_than {b} ) assume A3: a >= b ; ::_thesis: a is_>=_than {b} let c be Element of L; :: according to LATTICE3:def_9 ::_thesis: ( not c in {b} or c <= a ) thus ( not c in {b} or c <= a ) by A3, TARSKI:def_1; ::_thesis: verum end; theorem Th8: :: YELLOW_0:8 for L being RelStr for a, b, c being Element of L holds ( ( a is_<=_than {b,c} implies ( a <= b & a <= c ) ) & ( a <= b & a <= c implies a is_<=_than {b,c} ) & ( a is_>=_than {b,c} implies ( b <= a & c <= a ) ) & ( b <= a & c <= a implies a is_>=_than {b,c} ) ) proof let L be RelStr ; ::_thesis: for a, b, c being Element of L holds ( ( a is_<=_than {b,c} implies ( a <= b & a <= c ) ) & ( a <= b & a <= c implies a is_<=_than {b,c} ) & ( a is_>=_than {b,c} implies ( b <= a & c <= a ) ) & ( b <= a & c <= a implies a is_>=_than {b,c} ) ) let a, b, c be Element of L; ::_thesis: ( ( a is_<=_than {b,c} implies ( a <= b & a <= c ) ) & ( a <= b & a <= c implies a is_<=_than {b,c} ) & ( a is_>=_than {b,c} implies ( b <= a & c <= a ) ) & ( b <= a & c <= a implies a is_>=_than {b,c} ) ) A1: ( b in {b,c} & c in {b,c} ) by TARSKI:def_2; hence ( a is_<=_than {b,c} implies ( a <= b & a <= c ) ) by LATTICE3:def_8; ::_thesis: ( ( a <= b & a <= c implies a is_<=_than {b,c} ) & ( a is_>=_than {b,c} implies ( b <= a & c <= a ) ) & ( b <= a & c <= a implies a is_>=_than {b,c} ) ) hereby ::_thesis: ( a is_>=_than {b,c} iff ( b <= a & c <= a ) ) assume A2: ( a <= b & a <= c ) ; ::_thesis: a is_<=_than {b,c} thus a is_<=_than {b,c} ::_thesis: verum proof let c be Element of L; :: according to LATTICE3:def_8 ::_thesis: ( not c in {b,c} or a <= c ) thus ( not c in {b,c} or a <= c ) by A2, TARSKI:def_2; ::_thesis: verum end; end; thus ( a is_>=_than {b,c} implies ( a >= b & a >= c ) ) by A1, LATTICE3:def_9; ::_thesis: ( b <= a & c <= a implies a is_>=_than {b,c} ) assume A3: ( a >= b & a >= c ) ; ::_thesis: a is_>=_than {b,c} let c be Element of L; :: according to LATTICE3:def_9 ::_thesis: ( not c in {b,c} or c <= a ) thus ( not c in {b,c} or c <= a ) by A3, TARSKI:def_2; ::_thesis: verum end; theorem Th9: :: YELLOW_0:9 for L being RelStr for X, Y being set st X c= Y holds for x being Element of L holds ( ( x is_<=_than Y implies x is_<=_than X ) & ( x is_>=_than Y implies x is_>=_than X ) ) proof let L be RelStr ; ::_thesis: for X, Y being set st X c= Y holds for x being Element of L holds ( ( x is_<=_than Y implies x is_<=_than X ) & ( x is_>=_than Y implies x is_>=_than X ) ) let X, Y be set ; ::_thesis: ( X c= Y implies for x being Element of L holds ( ( x is_<=_than Y implies x is_<=_than X ) & ( x is_>=_than Y implies x is_>=_than X ) ) ) assume A1: X c= Y ; ::_thesis: for x being Element of L holds ( ( x is_<=_than Y implies x is_<=_than X ) & ( x is_>=_than Y implies x is_>=_than X ) ) let x be Element of L; ::_thesis: ( ( x is_<=_than Y implies x is_<=_than X ) & ( x is_>=_than Y implies x is_>=_than X ) ) thus ( x is_<=_than Y implies x is_<=_than X ) ::_thesis: ( x is_>=_than Y implies x is_>=_than X ) proof assume A2: for y being Element of L st y in Y holds y >= x ; :: according to LATTICE3:def_8 ::_thesis: x is_<=_than X let y be Element of L; :: according to LATTICE3:def_8 ::_thesis: ( not y in X or x <= y ) thus ( not y in X or x <= y ) by A1, A2; ::_thesis: verum end; assume A3: for y being Element of L st y in Y holds y <= x ; :: according to LATTICE3:def_9 ::_thesis: x is_>=_than X let y be Element of L; :: according to LATTICE3:def_9 ::_thesis: ( not y in X or y <= x ) thus ( not y in X or y <= x ) by A1, A3; ::_thesis: verum end; theorem Th10: :: YELLOW_0:10 for L being RelStr for X, Y being set for x being Element of L holds ( ( x is_<=_than X & x is_<=_than Y implies x is_<=_than X \/ Y ) & ( x is_>=_than X & x is_>=_than Y implies x is_>=_than X \/ Y ) ) proof let L be RelStr ; ::_thesis: for X, Y being set for x being Element of L holds ( ( x is_<=_than X & x is_<=_than Y implies x is_<=_than X \/ Y ) & ( x is_>=_than X & x is_>=_than Y implies x is_>=_than X \/ Y ) ) let X, Y be set ; ::_thesis: for x being Element of L holds ( ( x is_<=_than X & x is_<=_than Y implies x is_<=_than X \/ Y ) & ( x is_>=_than X & x is_>=_than Y implies x is_>=_than X \/ Y ) ) let x be Element of L; ::_thesis: ( ( x is_<=_than X & x is_<=_than Y implies x is_<=_than X \/ Y ) & ( x is_>=_than X & x is_>=_than Y implies x is_>=_than X \/ Y ) ) thus ( x is_<=_than X & x is_<=_than Y implies x is_<=_than X \/ Y ) ::_thesis: ( x is_>=_than X & x is_>=_than Y implies x is_>=_than X \/ Y ) proof assume A1: ( ( for y being Element of L st y in X holds y >= x ) & ( for y being Element of L st y in Y holds y >= x ) ) ; :: according to LATTICE3:def_8 ::_thesis: x is_<=_than X \/ Y let y be Element of L; :: according to LATTICE3:def_8 ::_thesis: ( not y in X \/ Y or x <= y ) ( not y in X \/ Y or y in X or y in Y ) by XBOOLE_0:def_3; hence ( not y in X \/ Y or x <= y ) by A1; ::_thesis: verum end; assume A2: ( ( for y being Element of L st y in X holds y <= x ) & ( for y being Element of L st y in Y holds y <= x ) ) ; :: according to LATTICE3:def_9 ::_thesis: x is_>=_than X \/ Y let y be Element of L; :: according to LATTICE3:def_9 ::_thesis: ( not y in X \/ Y or y <= x ) ( not y in X \/ Y or y in X or y in Y ) by XBOOLE_0:def_3; hence ( not y in X \/ Y or y <= x ) by A2; ::_thesis: verum end; theorem Th11: :: YELLOW_0:11 for L being transitive RelStr for X being set for x, y being Element of L st X is_<=_than x & x <= y holds X is_<=_than y proof let L be transitive RelStr ; ::_thesis: for X being set for x, y being Element of L st X is_<=_than x & x <= y holds X is_<=_than y let X be set ; ::_thesis: for x, y being Element of L st X is_<=_than x & x <= y holds X is_<=_than y let x, y be Element of L; ::_thesis: ( X is_<=_than x & x <= y implies X is_<=_than y ) assume that A1: for y being Element of L st y in X holds y <= x and A2: x <= y ; :: according to LATTICE3:def_9 ::_thesis: X is_<=_than y let z be Element of L; :: according to LATTICE3:def_9 ::_thesis: ( not z in X or z <= y ) assume z in X ; ::_thesis: z <= y then z <= x by A1; hence z <= y by A2, ORDERS_2:3; ::_thesis: verum end; theorem Th12: :: YELLOW_0:12 for L being transitive RelStr for X being set for x, y being Element of L st X is_>=_than x & x >= y holds X is_>=_than y proof let L be transitive RelStr ; ::_thesis: for X being set for x, y being Element of L st X is_>=_than x & x >= y holds X is_>=_than y let X be set ; ::_thesis: for x, y being Element of L st X is_>=_than x & x >= y holds X is_>=_than y let x, y be Element of L; ::_thesis: ( X is_>=_than x & x >= y implies X is_>=_than y ) assume that A1: for y being Element of L st y in X holds y >= x and A2: x >= y ; :: according to LATTICE3:def_8 ::_thesis: X is_>=_than y let z be Element of L; :: according to LATTICE3:def_8 ::_thesis: ( not z in X or y <= z ) assume z in X ; ::_thesis: y <= z then z >= x by A1; hence y <= z by A2, ORDERS_2:3; ::_thesis: verum end; registration let L be non empty RelStr ; cluster [#] L -> non empty ; coherence not [#] L is empty ; end; begin definition let L be RelStr ; attrL is lower-bounded means :Def4: :: YELLOW_0:def 4 ex x being Element of L st x is_<=_than the carrier of L; attrL is upper-bounded means :Def5: :: YELLOW_0:def 5 ex x being Element of L st x is_>=_than the carrier of L; end; :: deftheorem Def4 defines lower-bounded YELLOW_0:def_4_:_ for L being RelStr holds ( L is lower-bounded iff ex x being Element of L st x is_<=_than the carrier of L ); :: deftheorem Def5 defines upper-bounded YELLOW_0:def_5_:_ for L being RelStr holds ( L is upper-bounded iff ex x being Element of L st x is_>=_than the carrier of L ); definition let L be RelStr ; attrL is bounded means :: YELLOW_0:def 6 ( L is lower-bounded & L is upper-bounded ); end; :: deftheorem defines bounded YELLOW_0:def_6_:_ for L being RelStr holds ( L is bounded iff ( L is lower-bounded & L is upper-bounded ) ); theorem :: YELLOW_0:13 for P1, P2 being RelStr st RelStr(# the carrier of P1, the InternalRel of P1 #) = RelStr(# the carrier of P2, the InternalRel of P2 #) holds ( ( P1 is lower-bounded implies P2 is lower-bounded ) & ( P1 is upper-bounded implies P2 is upper-bounded ) ) proof let P1, P2 be RelStr ; ::_thesis: ( RelStr(# the carrier of P1, the InternalRel of P1 #) = RelStr(# the carrier of P2, the InternalRel of P2 #) implies ( ( P1 is lower-bounded implies P2 is lower-bounded ) & ( P1 is upper-bounded implies P2 is upper-bounded ) ) ) assume A1: RelStr(# the carrier of P1, the InternalRel of P1 #) = RelStr(# the carrier of P2, the InternalRel of P2 #) ; ::_thesis: ( ( P1 is lower-bounded implies P2 is lower-bounded ) & ( P1 is upper-bounded implies P2 is upper-bounded ) ) thus ( P1 is lower-bounded implies P2 is lower-bounded ) ::_thesis: ( P1 is upper-bounded implies P2 is upper-bounded ) proof given x being Element of P1 such that A2: x is_<=_than the carrier of P1 ; :: according to YELLOW_0:def_4 ::_thesis: P2 is lower-bounded reconsider y = x as Element of P2 by A1; take y ; :: according to YELLOW_0:def_4 ::_thesis: y is_<=_than the carrier of P2 thus y is_<=_than the carrier of P2 by A1, A2, Th2; ::_thesis: verum end; given x being Element of P1 such that A3: x is_>=_than the carrier of P1 ; :: according to YELLOW_0:def_5 ::_thesis: P2 is upper-bounded reconsider y = x as Element of P2 by A1; take y ; :: according to YELLOW_0:def_5 ::_thesis: y is_>=_than the carrier of P2 thus y is_>=_than the carrier of P2 by A1, A3, Th2; ::_thesis: verum end; registration cluster non empty complete -> non empty bounded for RelStr ; coherence for b1 being non empty RelStr st b1 is complete holds b1 is bounded proof let L be non empty RelStr ; ::_thesis: ( L is complete implies L is bounded ) assume A1: for X being set ex a being Element of L st ( X is_<=_than a & ( for b being Element of L st X is_<=_than b holds a <= b ) ) ; :: according to LATTICE3:def_12 ::_thesis: L is bounded then consider a0 being Element of L such that {} is_<=_than a0 and A2: for b being Element of L st {} is_<=_than b holds a0 <= b ; consider a1 being Element of L such that A3: the carrier of L is_<=_than a1 and for b being Element of L st the carrier of L is_<=_than b holds a1 <= b by A1; reconsider a0 = a0, a1 = a1 as Element of L ; hereby :: according to YELLOW_0:def_4,YELLOW_0:def_6 ::_thesis: L is upper-bounded take a0 = a0; ::_thesis: a0 is_<=_than the carrier of L thus a0 is_<=_than the carrier of L ::_thesis: verum proof let b be Element of L; :: according to LATTICE3:def_8 ::_thesis: ( not b in the carrier of L or a0 <= b ) thus ( not b in the carrier of L or a0 <= b ) by A2, Th6; ::_thesis: verum end; end; take a1 ; :: according to YELLOW_0:def_5 ::_thesis: a1 is_>=_than the carrier of L thus a1 is_>=_than the carrier of L by A3; ::_thesis: verum end; cluster bounded -> lower-bounded upper-bounded for RelStr ; coherence for b1 being RelStr st b1 is bounded holds ( b1 is lower-bounded & b1 is upper-bounded ) proof let L be RelStr ; ::_thesis: ( L is bounded implies ( L is lower-bounded & L is upper-bounded ) ) assume ( L is lower-bounded & L is upper-bounded ) ; :: according to YELLOW_0:def_6 ::_thesis: ( L is lower-bounded & L is upper-bounded ) hence ( L is lower-bounded & L is upper-bounded ) ; ::_thesis: verum end; cluster lower-bounded upper-bounded -> bounded for RelStr ; coherence for b1 being RelStr st b1 is lower-bounded & b1 is upper-bounded holds b1 is bounded proof let L be RelStr ; ::_thesis: ( L is lower-bounded & L is upper-bounded implies L is bounded ) assume ( L is lower-bounded & L is upper-bounded ) ; ::_thesis: L is bounded hence ( L is lower-bounded & L is upper-bounded ) ; :: according to YELLOW_0:def_6 ::_thesis: verum end; end; registration cluster non empty V136() reflexive transitive antisymmetric complete for RelStr ; existence ex b1 being non empty Poset st b1 is complete proof set L = the non empty complete Poset; take the non empty complete Poset ; ::_thesis: the non empty complete Poset is complete thus the non empty complete Poset is complete ; ::_thesis: verum end; end; definition let L be RelStr ; let X be set ; pred ex_sup_of X,L means :Def7: :: YELLOW_0:def 7 ex a being Element of L st ( X is_<=_than a & ( for b being Element of L st X is_<=_than b holds b >= a ) & ( for c being Element of L st X is_<=_than c & ( for b being Element of L st X is_<=_than b holds b >= c ) holds c = a ) ); pred ex_inf_of X,L means :Def8: :: YELLOW_0:def 8 ex a being Element of L st ( X is_>=_than a & ( for b being Element of L st X is_>=_than b holds b <= a ) & ( for c being Element of L st X is_>=_than c & ( for b being Element of L st X is_>=_than b holds b <= c ) holds c = a ) ); end; :: deftheorem Def7 defines ex_sup_of YELLOW_0:def_7_:_ for L being RelStr for X being set holds ( ex_sup_of X,L iff ex a being Element of L st ( X is_<=_than a & ( for b being Element of L st X is_<=_than b holds b >= a ) & ( for c being Element of L st X is_<=_than c & ( for b being Element of L st X is_<=_than b holds b >= c ) holds c = a ) ) ); :: deftheorem Def8 defines ex_inf_of YELLOW_0:def_8_:_ for L being RelStr for X being set holds ( ex_inf_of X,L iff ex a being Element of L st ( X is_>=_than a & ( for b being Element of L st X is_>=_than b holds b <= a ) & ( for c being Element of L st X is_>=_than c & ( for b being Element of L st X is_>=_than b holds b <= c ) holds c = a ) ) ); theorem Th14: :: YELLOW_0:14 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 set holds ( ( ex_sup_of X,L1 implies ex_sup_of X,L2 ) & ( ex_inf_of X,L1 implies ex_inf_of X,L2 ) ) proof let L1, L2 be RelStr ; ::_thesis: ( RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) implies for X being set holds ( ( ex_sup_of X,L1 implies ex_sup_of X,L2 ) & ( ex_inf_of X,L1 implies ex_inf_of X,L2 ) ) ) assume A1: RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) ; ::_thesis: for X being set holds ( ( ex_sup_of X,L1 implies ex_sup_of X,L2 ) & ( ex_inf_of X,L1 implies ex_inf_of X,L2 ) ) let X be set ; ::_thesis: ( ( ex_sup_of X,L1 implies ex_sup_of X,L2 ) & ( ex_inf_of X,L1 implies ex_inf_of X,L2 ) ) thus ( ex_sup_of X,L1 implies ex_sup_of X,L2 ) ::_thesis: ( ex_inf_of X,L1 implies ex_inf_of X,L2 ) proof given a being Element of L1 such that A2: X is_<=_than a and A3: for b being Element of L1 st X is_<=_than b holds b >= a and A4: for c being Element of L1 st X is_<=_than c & ( for b being Element of L1 st X is_<=_than b holds b >= c ) holds c = a ; :: according to YELLOW_0:def_7 ::_thesis: ex_sup_of X,L2 reconsider a9 = a as Element of L2 by A1; take a9 ; :: according to YELLOW_0:def_7 ::_thesis: ( X is_<=_than a9 & ( for b being Element of L2 st X is_<=_than b holds b >= a9 ) & ( for c being Element of L2 st X is_<=_than c & ( for b being Element of L2 st X is_<=_than b holds b >= c ) holds c = a9 ) ) thus X is_<=_than a9 by A1, A2, Th2; ::_thesis: ( ( for b being Element of L2 st X is_<=_than b holds b >= a9 ) & ( for c being Element of L2 st X is_<=_than c & ( for b being Element of L2 st X is_<=_than b holds b >= c ) holds c = a9 ) ) hereby ::_thesis: for c being Element of L2 st X is_<=_than c & ( for b being Element of L2 st X is_<=_than b holds b >= c ) holds c = a9 let b9 be Element of L2; ::_thesis: ( X is_<=_than b9 implies b9 >= a9 ) reconsider b = b9 as Element of L1 by A1; assume X is_<=_than b9 ; ::_thesis: b9 >= a9 then b >= a by A1, A3, Th2; hence b9 >= a9 by A1, Th1; ::_thesis: verum end; let c9 be Element of L2; ::_thesis: ( X is_<=_than c9 & ( for b being Element of L2 st X is_<=_than b holds b >= c9 ) implies c9 = a9 ) reconsider c = c9 as Element of L1 by A1; assume X is_<=_than c9 ; ::_thesis: ( ex b being Element of L2 st ( X is_<=_than b & not b >= c9 ) or c9 = a9 ) then A5: X is_<=_than c by A1, Th2; assume A6: for b9 being Element of L2 st X is_<=_than b9 holds b9 >= c9 ; ::_thesis: c9 = a9 now__::_thesis:_for_b_being_Element_of_L1_st_X_is_<=_than_b_holds_ b_>=_c let b be Element of L1; ::_thesis: ( X is_<=_than b implies b >= c ) reconsider b9 = b as Element of L2 by A1; assume X is_<=_than b ; ::_thesis: b >= c then b9 >= c9 by A1, A6, Th2; hence b >= c by A1, Th1; ::_thesis: verum end; hence c9 = a9 by A4, A5; ::_thesis: verum end; given a being Element of L1 such that A7: X is_>=_than a and A8: for b being Element of L1 st X is_>=_than b holds b <= a and A9: for c being Element of L1 st X is_>=_than c & ( for b being Element of L1 st X is_>=_than b holds b <= c ) holds c = a ; :: according to YELLOW_0:def_8 ::_thesis: ex_inf_of X,L2 reconsider a9 = a as Element of L2 by A1; take a9 ; :: according to YELLOW_0:def_8 ::_thesis: ( X is_>=_than a9 & ( for b being Element of L2 st X is_>=_than b holds b <= a9 ) & ( for c being Element of L2 st X is_>=_than c & ( for b being Element of L2 st X is_>=_than b holds b <= c ) holds c = a9 ) ) thus X is_>=_than a9 by A1, A7, Th2; ::_thesis: ( ( for b being Element of L2 st X is_>=_than b holds b <= a9 ) & ( for c being Element of L2 st X is_>=_than c & ( for b being Element of L2 st X is_>=_than b holds b <= c ) holds c = a9 ) ) hereby ::_thesis: for c being Element of L2 st X is_>=_than c & ( for b being Element of L2 st X is_>=_than b holds b <= c ) holds c = a9 let b9 be Element of L2; ::_thesis: ( X is_>=_than b9 implies b9 <= a9 ) reconsider b = b9 as Element of L1 by A1; assume X is_>=_than b9 ; ::_thesis: b9 <= a9 then b <= a by A1, A8, Th2; hence b9 <= a9 by A1, Th1; ::_thesis: verum end; let c9 be Element of L2; ::_thesis: ( X is_>=_than c9 & ( for b being Element of L2 st X is_>=_than b holds b <= c9 ) implies c9 = a9 ) reconsider c = c9 as Element of L1 by A1; assume A10: X is_>=_than c9 ; ::_thesis: ( ex b being Element of L2 st ( X is_>=_than b & not b <= c9 ) or c9 = a9 ) assume A11: for b9 being Element of L2 st X is_>=_than b9 holds b9 <= c9 ; ::_thesis: c9 = a9 A12: now__::_thesis:_for_b_being_Element_of_L1_st_X_is_>=_than_b_holds_ b_<=_c let b be Element of L1; ::_thesis: ( X is_>=_than b implies b <= c ) reconsider b9 = b as Element of L2 by A1; assume X is_>=_than b ; ::_thesis: b <= c then b9 <= c9 by A1, A11, Th2; hence b <= c by A1, Th1; ::_thesis: verum end; X is_>=_than c by A1, A10, Th2; hence c9 = a9 by A9, A12; ::_thesis: verum end; theorem Th15: :: YELLOW_0:15 for L being antisymmetric RelStr for X being set holds ( ex_sup_of X,L iff ex a being Element of L st ( X is_<=_than a & ( for b being Element of L st X is_<=_than b holds a <= b ) ) ) proof let L be antisymmetric RelStr ; ::_thesis: for X being set holds ( ex_sup_of X,L iff ex a being Element of L st ( X is_<=_than a & ( for b being Element of L st X is_<=_than b holds a <= b ) ) ) let X be set ; ::_thesis: ( ex_sup_of X,L iff ex a being Element of L st ( X is_<=_than a & ( for b being Element of L st X is_<=_than b holds a <= b ) ) ) hereby ::_thesis: ( ex a being Element of L st ( X is_<=_than a & ( for b being Element of L st X is_<=_than b holds a <= b ) ) implies ex_sup_of X,L ) assume ex_sup_of X,L ; ::_thesis: ex a being Element of L st ( X is_<=_than a & ( for b being Element of L st X is_<=_than b holds a <= b ) ) then ex a being Element of L st ( X is_<=_than a & ( for b being Element of L st X is_<=_than b holds b >= a ) & ( for c being Element of L st X is_<=_than c & ( for b being Element of L st X is_<=_than b holds b >= c ) holds c = a ) ) by Def7; hence ex a being Element of L st ( X is_<=_than a & ( for b being Element of L st X is_<=_than b holds a <= b ) ) ; ::_thesis: verum end; given a being Element of L such that A1: ( X is_<=_than a & ( for b being Element of L st X is_<=_than b holds a <= b ) ) ; ::_thesis: ex_sup_of X,L take a ; :: according to YELLOW_0:def_7 ::_thesis: ( X is_<=_than a & ( for b being Element of L st X is_<=_than b holds b >= a ) & ( for c being Element of L st X is_<=_than c & ( for b being Element of L st X is_<=_than b holds b >= c ) holds c = a ) ) thus ( X is_<=_than a & ( for b being Element of L st X is_<=_than b holds b >= a ) ) by A1; ::_thesis: for c being Element of L st X is_<=_than c & ( for b being Element of L st X is_<=_than b holds b >= c ) holds c = a let c be Element of L; ::_thesis: ( X is_<=_than c & ( for b being Element of L st X is_<=_than b holds b >= c ) implies c = a ) assume ( X is_<=_than c & ( for b being Element of L st X is_<=_than b holds b >= c ) ) ; ::_thesis: c = a then ( a <= c & c <= a ) by A1; hence c = a by ORDERS_2:2; ::_thesis: verum end; theorem Th16: :: YELLOW_0:16 for L being antisymmetric RelStr for X being set holds ( ex_inf_of X,L iff ex a being Element of L st ( X is_>=_than a & ( for b being Element of L st X is_>=_than b holds a >= b ) ) ) proof let L be antisymmetric RelStr ; ::_thesis: for X being set holds ( ex_inf_of X,L iff ex a being Element of L st ( X is_>=_than a & ( for b being Element of L st X is_>=_than b holds a >= b ) ) ) let X be set ; ::_thesis: ( ex_inf_of X,L iff ex a being Element of L st ( X is_>=_than a & ( for b being Element of L st X is_>=_than b holds a >= b ) ) ) hereby ::_thesis: ( ex a being Element of L st ( X is_>=_than a & ( for b being Element of L st X is_>=_than b holds a >= b ) ) implies ex_inf_of X,L ) assume ex_inf_of X,L ; ::_thesis: ex a being Element of L st ( X is_>=_than a & ( for b being Element of L st X is_>=_than b holds a >= b ) ) then ex a being Element of L st ( X is_>=_than a & ( for b being Element of L st X is_>=_than b holds b <= a ) & ( for c being Element of L st X is_>=_than c & ( for b being Element of L st X is_>=_than b holds b <= c ) holds c = a ) ) by Def8; hence ex a being Element of L st ( X is_>=_than a & ( for b being Element of L st X is_>=_than b holds a >= b ) ) ; ::_thesis: verum end; given a being Element of L such that A1: ( X is_>=_than a & ( for b being Element of L st X is_>=_than b holds a >= b ) ) ; ::_thesis: ex_inf_of X,L take a ; :: according to YELLOW_0:def_8 ::_thesis: ( X is_>=_than a & ( for b being Element of L st X is_>=_than b holds b <= a ) & ( for c being Element of L st X is_>=_than c & ( for b being Element of L st X is_>=_than b holds b <= c ) holds c = a ) ) thus ( X is_>=_than a & ( for b being Element of L st X is_>=_than b holds a >= b ) ) by A1; ::_thesis: for c being Element of L st X is_>=_than c & ( for b being Element of L st X is_>=_than b holds b <= c ) holds c = a let c be Element of L; ::_thesis: ( X is_>=_than c & ( for b being Element of L st X is_>=_than b holds b <= c ) implies c = a ) assume ( X is_>=_than c & ( for b being Element of L st X is_>=_than b holds c >= b ) ) ; ::_thesis: c = a then ( a <= c & c <= a ) by A1; hence c = a by ORDERS_2:2; ::_thesis: verum end; theorem Th17: :: YELLOW_0:17 for L being non empty antisymmetric complete RelStr for X being set holds ( ex_sup_of X,L & ex_inf_of X,L ) proof let L be non empty antisymmetric complete RelStr ; ::_thesis: for X being set holds ( ex_sup_of X,L & ex_inf_of X,L ) let X be set ; ::_thesis: ( ex_sup_of X,L & ex_inf_of X,L ) set Y = { c where c is Element of L : c is_<=_than X } ; consider a being Element of L such that A1: { c where c is Element of L : c is_<=_than X } is_<=_than a and A2: for b being Element of L st { c where c is Element of L : c is_<=_than X } is_<=_than b holds a <= b by LATTICE3:def_12; ex a being Element of L st ( X is_<=_than a & ( for b being Element of L st X is_<=_than b holds a <= b ) ) by LATTICE3:def_12; hence ex_sup_of X,L by Th15; ::_thesis: ex_inf_of X,L now__::_thesis:_ex_a_being_Element_of_L_st_ (_a_is_<=_than_X_&_(_for_b_being_Element_of_L_st_b_is_<=_than_X_holds_ b_<=_a_)_) take a = a; ::_thesis: ( a is_<=_than X & ( for b being Element of L st b is_<=_than X holds b <= a ) ) thus a is_<=_than X ::_thesis: for b being Element of L st b is_<=_than X holds b <= a proof let b be Element of L; :: according to LATTICE3:def_8 ::_thesis: ( not b in X or a <= b ) assume A3: b in X ; ::_thesis: a <= b { c where c is Element of L : c is_<=_than X } is_<=_than b proof let c be Element of L; :: according to LATTICE3:def_9 ::_thesis: ( not c in { c where c is Element of L : c is_<=_than X } or c <= b ) assume c in { c where c is Element of L : c is_<=_than X } ; ::_thesis: c <= b then ex d being Element of L st ( c = d & d is_<=_than X ) ; hence c <= b by A3, LATTICE3:def_8; ::_thesis: verum end; hence a <= b by A2; ::_thesis: verum end; let b be Element of L; ::_thesis: ( b is_<=_than X implies b <= a ) assume b is_<=_than X ; ::_thesis: b <= a then b in { c where c is Element of L : c is_<=_than X } ; hence b <= a by A1, LATTICE3:def_9; ::_thesis: verum end; hence ex_inf_of X,L by Th16; ::_thesis: verum end; theorem Th18: :: YELLOW_0:18 for L being antisymmetric RelStr for a, b, c being Element of L holds ( c = a "\/" b & ex_sup_of {a,b},L iff ( c >= a & c >= b & ( for d being Element of L st d >= a & d >= b holds c <= d ) ) ) proof let L be antisymmetric RelStr ; ::_thesis: for a, b, c being Element of L holds ( c = a "\/" b & ex_sup_of {a,b},L iff ( c >= a & c >= b & ( for d being Element of L st d >= a & d >= b holds c <= d ) ) ) let a, b, c be Element of L; ::_thesis: ( c = a "\/" b & ex_sup_of {a,b},L iff ( c >= a & c >= b & ( for d being Element of L st d >= a & d >= b holds c <= d ) ) ) hereby ::_thesis: ( c >= a & c >= b & ( for d being Element of L st d >= a & d >= b holds c <= d ) implies ( c = a "\/" b & ex_sup_of {a,b},L ) ) assume that A1: c = a "\/" b and A2: ex_sup_of {a,b},L ; ::_thesis: ( c >= a & c >= b & ( for d being Element of L st d >= a & d >= b holds c <= d ) ) consider c1 being Element of L such that A3: {a,b} is_<=_than c1 and A4: for d being Element of L st {a,b} is_<=_than d holds c1 <= d by A2, Th15; A5: now__::_thesis:_for_d_being_Element_of_L_st_a_<=_d_&_b_<=_d_holds_ c1_<=_d let d be Element of L; ::_thesis: ( a <= d & b <= d implies c1 <= d ) assume ( a <= d & b <= d ) ; ::_thesis: c1 <= d then {a,b} is_<=_than d by Th8; hence c1 <= d by A4; ::_thesis: verum end; ( a <= c1 & b <= c1 ) by A3, Th8; hence ( c >= a & c >= b & ( for d being Element of L st d >= a & d >= b holds c <= d ) ) by A1, A5, LATTICE3:def_13; ::_thesis: verum end; assume that A6: ( c >= a & c >= b ) and A7: for d being Element of L st d >= a & d >= b holds c <= d ; ::_thesis: ( c = a "\/" b & ex_sup_of {a,b},L ) thus c = a "\/" b by A6, A7, LATTICE3:def_13; ::_thesis: ex_sup_of {a,b},L now__::_thesis:_ex_c_being_Element_of_L_st_ (_c_is_>=_than_{a,b}_&_(_for_d_being_Element_of_L_st_d_is_>=_than_{a,b}_holds_ c_<=_d_)_) take c = c; ::_thesis: ( c is_>=_than {a,b} & ( for d being Element of L st d is_>=_than {a,b} holds c <= d ) ) thus c is_>=_than {a,b} by A6, Th8; ::_thesis: for d being Element of L st d is_>=_than {a,b} holds c <= d let d be Element of L; ::_thesis: ( d is_>=_than {a,b} implies c <= d ) assume d is_>=_than {a,b} ; ::_thesis: c <= d then ( d >= a & d >= b ) by Th8; hence c <= d by A7; ::_thesis: verum end; hence ex_sup_of {a,b},L by Th15; ::_thesis: verum end; theorem Th19: :: YELLOW_0:19 for L being antisymmetric RelStr for a, b, c being Element of L holds ( c = a "/\" b & ex_inf_of {a,b},L iff ( c <= a & c <= b & ( for d being Element of L st d <= a & d <= b holds c >= d ) ) ) proof let L be antisymmetric RelStr ; ::_thesis: for a, b, c being Element of L holds ( c = a "/\" b & ex_inf_of {a,b},L iff ( c <= a & c <= b & ( for d being Element of L st d <= a & d <= b holds c >= d ) ) ) let a, b, c be Element of L; ::_thesis: ( c = a "/\" b & ex_inf_of {a,b},L iff ( c <= a & c <= b & ( for d being Element of L st d <= a & d <= b holds c >= d ) ) ) hereby ::_thesis: ( c <= a & c <= b & ( for d being Element of L st d <= a & d <= b holds c >= d ) implies ( c = a "/\" b & ex_inf_of {a,b},L ) ) assume that A1: c = a "/\" b and A2: ex_inf_of {a,b},L ; ::_thesis: ( c <= a & c <= b & ( for d being Element of L st d <= a & d <= b holds c >= d ) ) consider c1 being Element of L such that A3: {a,b} is_>=_than c1 and A4: for d being Element of L st {a,b} is_>=_than d holds c1 >= d by A2, Th16; A5: now__::_thesis:_for_d_being_Element_of_L_st_a_>=_d_&_b_>=_d_holds_ c1_>=_d let d be Element of L; ::_thesis: ( a >= d & b >= d implies c1 >= d ) assume ( a >= d & b >= d ) ; ::_thesis: c1 >= d then {a,b} is_>=_than d by Th8; hence c1 >= d by A4; ::_thesis: verum end; ( a >= c1 & b >= c1 ) by A3, Th8; hence ( c <= a & c <= b & ( for d being Element of L st d <= a & d <= b holds c >= d ) ) by A1, A5, LATTICE3:def_14; ::_thesis: verum end; assume that A6: ( c <= a & c <= b ) and A7: for d being Element of L st d <= a & d <= b holds c >= d ; ::_thesis: ( c = a "/\" b & ex_inf_of {a,b},L ) thus c = a "/\" b by A6, A7, LATTICE3:def_14; ::_thesis: ex_inf_of {a,b},L now__::_thesis:_ex_c_being_Element_of_L_st_ (_c_is_<=_than_{a,b}_&_(_for_d_being_Element_of_L_st_d_is_<=_than_{a,b}_holds_ c_>=_d_)_) take c = c; ::_thesis: ( c is_<=_than {a,b} & ( for d being Element of L st d is_<=_than {a,b} holds c >= d ) ) thus c is_<=_than {a,b} by A6, Th8; ::_thesis: for d being Element of L st d is_<=_than {a,b} holds c >= d let d be Element of L; ::_thesis: ( d is_<=_than {a,b} implies c >= d ) assume d is_<=_than {a,b} ; ::_thesis: c >= d then ( d <= a & d <= b ) by Th8; hence c >= d by A7; ::_thesis: verum end; hence ex_inf_of {a,b},L by Th16; ::_thesis: verum end; theorem Th20: :: YELLOW_0:20 for L being antisymmetric RelStr holds ( L is with_suprema iff for a, b being Element of L holds ex_sup_of {a,b},L ) proof let L be antisymmetric RelStr ; ::_thesis: ( L is with_suprema iff for a, b being Element of L holds ex_sup_of {a,b},L ) hereby ::_thesis: ( ( for a, b being Element of L holds ex_sup_of {a,b},L ) implies L is with_suprema ) assume A1: L is with_suprema ; ::_thesis: for a, b being Element of L holds ex_sup_of {a,b},L let a, b be Element of L; ::_thesis: ex_sup_of {a,b},L ex z being Element of L st ( a <= z & b <= z & ( for z9 being Element of L st a <= z9 & b <= z9 holds z <= z9 ) ) by A1, LATTICE3:def_10; hence ex_sup_of {a,b},L by Th18; ::_thesis: verum end; assume A2: for a, b being Element of L holds ex_sup_of {a,b},L ; ::_thesis: L is with_suprema let x, y be Element of L; :: according to LATTICE3:def_10 ::_thesis: ex b1 being Element of the carrier of L st ( x <= b1 & y <= b1 & ( for b2 being Element of the carrier of L holds ( not x <= b2 or not y <= b2 or b1 <= b2 ) ) ) take x "\/" y ; ::_thesis: ( x <= x "\/" y & y <= x "\/" y & ( for b1 being Element of the carrier of L holds ( not x <= b1 or not y <= b1 or x "\/" y <= b1 ) ) ) ex_sup_of {x,y},L by A2; hence ( x <= x "\/" y & y <= x "\/" y & ( for b1 being Element of the carrier of L holds ( not x <= b1 or not y <= b1 or x "\/" y <= b1 ) ) ) by Th18; ::_thesis: verum end; theorem Th21: :: YELLOW_0:21 for L being antisymmetric RelStr holds ( L is with_infima iff for a, b being Element of L holds ex_inf_of {a,b},L ) proof let L be antisymmetric RelStr ; ::_thesis: ( L is with_infima iff for a, b being Element of L holds ex_inf_of {a,b},L ) hereby ::_thesis: ( ( for a, b being Element of L holds ex_inf_of {a,b},L ) implies L is with_infima ) assume A1: L is with_infima ; ::_thesis: for a, b being Element of L holds ex_inf_of {a,b},L let a, b be Element of L; ::_thesis: ex_inf_of {a,b},L ex z being Element of L st ( a >= z & b >= z & ( for z9 being Element of L st a >= z9 & b >= z9 holds z >= z9 ) ) by A1, LATTICE3:def_11; hence ex_inf_of {a,b},L by Th19; ::_thesis: verum end; assume A2: for a, b being Element of L holds ex_inf_of {a,b},L ; ::_thesis: L is with_infima let x, y be Element of L; :: according to LATTICE3:def_11 ::_thesis: ex b1 being Element of the carrier of L st ( b1 <= x & b1 <= y & ( for b2 being Element of the carrier of L holds ( not b2 <= x or not b2 <= y or b2 <= b1 ) ) ) take x "/\" y ; ::_thesis: ( x "/\" y <= x & x "/\" y <= y & ( for b1 being Element of the carrier of L holds ( not b1 <= x or not b1 <= y or b1 <= x "/\" y ) ) ) ex_inf_of {x,y},L by A2; hence ( x "/\" y <= x & x "/\" y <= y & ( for b1 being Element of the carrier of L holds ( not b1 <= x or not b1 <= y or b1 <= x "/\" y ) ) ) by Th19; ::_thesis: verum end; theorem Th22: :: YELLOW_0:22 for L being antisymmetric with_suprema RelStr for a, b, c being Element of L holds ( c = a "\/" b iff ( c >= a & c >= b & ( for d being Element of L st d >= a & d >= b holds c <= d ) ) ) proof let A be antisymmetric with_suprema RelStr ; ::_thesis: for a, b, c being Element of A holds ( c = a "\/" b iff ( c >= a & c >= b & ( for d being Element of A st d >= a & d >= b holds c <= d ) ) ) let a, b be Element of A; ::_thesis: for c being Element of A holds ( c = a "\/" b iff ( c >= a & c >= b & ( for d being Element of A st d >= a & d >= b holds c <= d ) ) ) ex x being Element of A st ( a <= x & b <= x & ( for c being Element of A st a <= c & b <= c holds x <= c ) ) by LATTICE3:def_10; hence for c being Element of A holds ( c = a "\/" b iff ( c >= a & c >= b & ( for d being Element of A st d >= a & d >= b holds c <= d ) ) ) by LATTICE3:def_13; ::_thesis: verum end; theorem Th23: :: YELLOW_0:23 for L being antisymmetric with_infima RelStr for a, b, c being Element of L holds ( c = a "/\" b iff ( c <= a & c <= b & ( for d being Element of L st d <= a & d <= b holds c >= d ) ) ) proof let A be antisymmetric with_infima RelStr ; ::_thesis: for a, b, c being Element of A holds ( c = a "/\" b iff ( c <= a & c <= b & ( for d being Element of A st d <= a & d <= b holds c >= d ) ) ) let a, b be Element of A; ::_thesis: for c being Element of A holds ( c = a "/\" b iff ( c <= a & c <= b & ( for d being Element of A st d <= a & d <= b holds c >= d ) ) ) ex x being Element of A st ( a >= x & b >= x & ( for c being Element of A st a >= c & b >= c holds x >= c ) ) by LATTICE3:def_11; hence for c being Element of A holds ( c = a "/\" b iff ( c <= a & c <= b & ( for d being Element of A st d <= a & d <= b holds c >= d ) ) ) by LATTICE3:def_14; ::_thesis: verum end; theorem :: YELLOW_0:24 for L being reflexive antisymmetric with_suprema RelStr for a, b being Element of L holds ( a = a "\/" b iff a >= b ) proof let L be reflexive antisymmetric with_suprema RelStr ; ::_thesis: for a, b being Element of L holds ( a = a "\/" b iff a >= b ) let a, b be Element of L; ::_thesis: ( a = a "\/" b iff a >= b ) ( a <= a & ( for d being Element of L st d >= a & d >= b holds a <= d ) ) ; hence ( a = a "\/" b iff a >= b ) by Th22; ::_thesis: verum end; theorem :: YELLOW_0:25 for L being reflexive antisymmetric with_infima RelStr for a, b being Element of L holds ( a = a "/\" b iff a <= b ) proof let L be reflexive antisymmetric with_infima RelStr ; ::_thesis: for a, b being Element of L holds ( a = a "/\" b iff a <= b ) let a, b be Element of L; ::_thesis: ( a = a "/\" b iff a <= b ) ( a <= a & ( for d being Element of L st d <= a & d <= b holds a >= d ) ) ; hence ( a = a "/\" b iff a <= b ) by Th23; ::_thesis: verum end; definition let L be RelStr ; let X be set ; func "\/" (X,L) -> Element of L means :Def9: :: YELLOW_0:def 9 ( X is_<=_than it & ( for a being Element of L st X is_<=_than a holds it <= a ) ) if ex_sup_of X,L ; uniqueness for b1, b2 being Element of L st ex_sup_of X,L & X is_<=_than b1 & ( for a being Element of L st X is_<=_than a holds b1 <= a ) & X is_<=_than b2 & ( for a being Element of L st X is_<=_than a holds b2 <= a ) holds b1 = b2 proof let a1, a2 be Element of L; ::_thesis: ( ex_sup_of X,L & X is_<=_than a1 & ( for a being Element of L st X is_<=_than a holds a1 <= a ) & X is_<=_than a2 & ( for a being Element of L st X is_<=_than a holds a2 <= a ) implies a1 = a2 ) given a being Element of L such that X is_<=_than a and for b being Element of L st X is_<=_than b holds b >= a and A1: for c being Element of L st X is_<=_than c & ( for b being Element of L st X is_<=_than b holds b >= c ) holds c = a ; :: according to YELLOW_0:def_7 ::_thesis: ( not X is_<=_than a1 or ex a being Element of L st ( X is_<=_than a & not a1 <= a ) or not X is_<=_than a2 or ex a being Element of L st ( X is_<=_than a & not a2 <= a ) or a1 = a2 ) assume A2: ( X is_<=_than a1 & ( for a being Element of L st X is_<=_than a holds a1 <= a ) & X is_<=_than a2 & ( for a being Element of L st X is_<=_than a holds a2 <= a ) & not a1 = a2 ) ; ::_thesis: contradiction then a1 = a by A1; hence contradiction by A1, A2; ::_thesis: verum end; existence ( ex_sup_of X,L implies ex b1 being Element of L st ( X is_<=_than b1 & ( for a being Element of L st X is_<=_than a holds b1 <= a ) ) ) proof ( ex_sup_of X,L implies ex a being Element of L st ( X is_<=_than a & ( for b being Element of L st X is_<=_than b holds b >= a ) & ( for c being Element of L st X is_<=_than c & ( for b being Element of L st X is_<=_than b holds b >= c ) holds c = a ) ) ) by Def7; hence ( ex_sup_of X,L implies ex b1 being Element of L st ( X is_<=_than b1 & ( for a being Element of L st X is_<=_than a holds b1 <= a ) ) ) ; ::_thesis: verum end; correctness consistency for b1 being Element of L holds verum; ; func "/\" (X,L) -> Element of L means :Def10: :: YELLOW_0:def 10 ( X is_>=_than it & ( for a being Element of L st X is_>=_than a holds a <= it ) ) if ex_inf_of X,L ; uniqueness for b1, b2 being Element of L st ex_inf_of X,L & X is_>=_than b1 & ( for a being Element of L st X is_>=_than a holds a <= b1 ) & X is_>=_than b2 & ( for a being Element of L st X is_>=_than a holds a <= b2 ) holds b1 = b2 proof let a1, a2 be Element of L; ::_thesis: ( ex_inf_of X,L & X is_>=_than a1 & ( for a being Element of L st X is_>=_than a holds a <= a1 ) & X is_>=_than a2 & ( for a being Element of L st X is_>=_than a holds a <= a2 ) implies a1 = a2 ) given a being Element of L such that X is_>=_than a and for b being Element of L st X is_>=_than b holds b <= a and A3: for c being Element of L st X is_>=_than c & ( for b being Element of L st X is_>=_than b holds b <= c ) holds c = a ; :: according to YELLOW_0:def_8 ::_thesis: ( not X is_>=_than a1 or ex a being Element of L st ( X is_>=_than a & not a <= a1 ) or not X is_>=_than a2 or ex a being Element of L st ( X is_>=_than a & not a <= a2 ) or a1 = a2 ) assume A4: ( X is_>=_than a1 & ( for a being Element of L st X is_>=_than a holds a <= a1 ) & X is_>=_than a2 & ( for a being Element of L st X is_>=_than a holds a <= a2 ) & not a1 = a2 ) ; ::_thesis: contradiction then a1 = a by A3; hence contradiction by A3, A4; ::_thesis: verum end; existence ( ex_inf_of X,L implies ex b1 being Element of L st ( X is_>=_than b1 & ( for a being Element of L st X is_>=_than a holds a <= b1 ) ) ) proof ( ex_inf_of X,L implies ex a being Element of L st ( X is_>=_than a & ( for b being Element of L st X is_>=_than b holds b <= a ) & ( for c being Element of L st X is_>=_than c & ( for b being Element of L st X is_>=_than b holds b <= c ) holds c = a ) ) ) by Def8; hence ( ex_inf_of X,L implies ex b1 being Element of L st ( X is_>=_than b1 & ( for a being Element of L st X is_>=_than a holds a <= b1 ) ) ) ; ::_thesis: verum end; correctness consistency for b1 being Element of L holds verum; ; end; :: deftheorem Def9 defines "\/" YELLOW_0:def_9_:_ for L being RelStr for X being set for b3 being Element of L st ex_sup_of X,L holds ( b3 = "\/" (X,L) iff ( X is_<=_than b3 & ( for a being Element of L st X is_<=_than a holds b3 <= a ) ) ); :: deftheorem Def10 defines "/\" YELLOW_0:def_10_:_ for L being RelStr for X being set for b3 being Element of L st ex_inf_of X,L holds ( b3 = "/\" (X,L) iff ( X is_>=_than b3 & ( for a being Element of L st X is_>=_than a holds a <= b3 ) ) ); theorem :: YELLOW_0:26 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 set st ex_sup_of X,L1 holds "\/" (X,L1) = "\/" (X,L2) proof let L1, L2 be RelStr ; ::_thesis: ( RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) implies for X being set st ex_sup_of X,L1 holds "\/" (X,L1) = "\/" (X,L2) ) assume A1: RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) ; ::_thesis: for X being set st ex_sup_of X,L1 holds "\/" (X,L1) = "\/" (X,L2) let X be set ; ::_thesis: ( ex_sup_of X,L1 implies "\/" (X,L1) = "\/" (X,L2) ) reconsider c = "\/" (X,L1) as Element of L2 by A1; assume A2: ex_sup_of X,L1 ; ::_thesis: "\/" (X,L1) = "\/" (X,L2) then X is_<=_than "\/" (X,L1) by Def9; then A3: X is_<=_than c by A1, Th2; A4: now__::_thesis:_for_a_being_Element_of_L2_st_X_is_<=_than_a_holds_ a_>=_c let a be Element of L2; ::_thesis: ( X is_<=_than a implies a >= c ) reconsider b = a as Element of L1 by A1; assume X is_<=_than a ; ::_thesis: a >= c then X is_<=_than b by A1, Th2; then b >= "\/" (X,L1) by A2, Def9; hence a >= c by A1, Th1; ::_thesis: verum end; ex_sup_of X,L2 by A1, A2, Th14; hence "\/" (X,L1) = "\/" (X,L2) by A3, A4, Def9; ::_thesis: verum end; theorem :: YELLOW_0:27 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 set st ex_inf_of X,L1 holds "/\" (X,L1) = "/\" (X,L2) proof let L1, L2 be RelStr ; ::_thesis: ( RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) implies for X being set st ex_inf_of X,L1 holds "/\" (X,L1) = "/\" (X,L2) ) assume A1: RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) ; ::_thesis: for X being set st ex_inf_of X,L1 holds "/\" (X,L1) = "/\" (X,L2) let X be set ; ::_thesis: ( ex_inf_of X,L1 implies "/\" (X,L1) = "/\" (X,L2) ) reconsider c = "/\" (X,L1) as Element of L2 by A1; assume A2: ex_inf_of X,L1 ; ::_thesis: "/\" (X,L1) = "/\" (X,L2) then X is_>=_than "/\" (X,L1) by Def10; then A3: X is_>=_than c by A1, Th2; A4: now__::_thesis:_for_a_being_Element_of_L2_st_X_is_>=_than_a_holds_ a_<=_c let a be Element of L2; ::_thesis: ( X is_>=_than a implies a <= c ) reconsider b = a as Element of L1 by A1; assume X is_>=_than a ; ::_thesis: a <= c then X is_>=_than b by A1, Th2; then b <= "/\" (X,L1) by A2, Def10; hence a <= c by A1, Th1; ::_thesis: verum end; ex_inf_of X,L2 by A1, A2, Th14; hence "/\" (X,L1) = "/\" (X,L2) by A3, A4, Def10; ::_thesis: verum end; theorem :: YELLOW_0:28 for L being non empty complete Poset for X being set holds ( "\/" (X,L) = "\/" (X,(latt L)) & "/\" (X,L) = "/\" (X,(latt L)) ) proof let L be non empty complete Poset; ::_thesis: for X being set holds ( "\/" (X,L) = "\/" (X,(latt L)) & "/\" (X,L) = "/\" (X,(latt L)) ) let X be set ; ::_thesis: ( "\/" (X,L) = "\/" (X,(latt L)) & "/\" (X,L) = "/\" (X,(latt L)) ) A1: RelStr(# the carrier of L, the InternalRel of L #) = LattPOSet (latt L) by LATTICE3:def_15; then reconsider x = "\/" (X,L) as Element of (LattPOSet (latt L)) ; reconsider y = "/\" (X,(latt L)) as Element of L by A1; A2: now__::_thesis:_for_a_being_Element_of_L_st_a_is_<=_than_X_holds_ a_<=_y let a be Element of L; ::_thesis: ( a is_<=_than X implies a <= y ) reconsider a9 = a as Element of (LattPOSet (latt L)) by A1; assume a is_<=_than X ; ::_thesis: a <= y then a9 is_<=_than X by A1, Th2; then % a9 is_less_than X by LATTICE3:29; then A3: % a9 [= "/\" (X,(latt L)) by LATTICE3:34; (% a9) % = % a9 ; then a9 <= ("/\" (X,(latt L))) % by A3, LATTICE3:7; hence a <= y by A1, Th1; ::_thesis: verum end; ex a being Element of L st ( X is_<=_than a & ( for b being Element of L st X is_<=_than b holds a <= b ) ) by LATTICE3:def_12; then A4: ex_sup_of X,L by Th15; A5: now__::_thesis:_for_a_being_Element_of_(latt_L)_st_X_is_less_than_a_holds_ %_x_[=_a let a be Element of (latt L); ::_thesis: ( X is_less_than a implies % x [= a ) reconsider a9 = a % as Element of L by A1; assume X is_less_than a ; ::_thesis: % x [= a then X is_<=_than a % by LATTICE3:30; then X is_<=_than a9 by A1, Th2; then "\/" (X,L) <= a9 by A4, Def9; then A6: x <= a % by A1, Th1; (% x) % = % x ; hence % x [= a by A6, LATTICE3:7; ::_thesis: verum end; X is_<=_than "\/" (X,L) by A4, Def9; then X is_<=_than x by A1, Th2; then X is_less_than % x by LATTICE3:31; hence "\/" (X,L) = "\/" (X,(latt L)) by A5, LATTICE3:def_21; ::_thesis: "/\" (X,L) = "/\" (X,(latt L)) "/\" (X,(latt L)) is_less_than X by LATTICE3:34; then ("/\" (X,(latt L))) % is_<=_than X by LATTICE3:28; then A7: y is_<=_than X by A1, Th2; then ex_inf_of X,L by A2, Th16; hence "/\" (X,L) = "/\" (X,(latt L)) by A7, A2, Def10; ::_thesis: verum end; theorem :: YELLOW_0:29 for L being complete Lattice for X being set holds ( "\/" (X,L) = "\/" (X,(LattPOSet L)) & "/\" (X,L) = "/\" (X,(LattPOSet L)) ) proof let L be complete Lattice; ::_thesis: for X being set holds ( "\/" (X,L) = "\/" (X,(LattPOSet L)) & "/\" (X,L) = "/\" (X,(LattPOSet L)) ) let X be set ; ::_thesis: ( "\/" (X,L) = "\/" (X,(LattPOSet L)) & "/\" (X,L) = "/\" (X,(LattPOSet L)) ) A1: now__::_thesis:_for_r_being_Element_of_(LattPOSet_L)_st_X_is_<=_than_r_holds_ ("\/"_(X,L))_%_<=_r let r be Element of (LattPOSet L); ::_thesis: ( X is_<=_than r implies ("\/" (X,L)) % <= r ) assume X is_<=_than r ; ::_thesis: ("\/" (X,L)) % <= r then X is_less_than % r by LATTICE3:31; then A2: "\/" (X,L) [= % r by LATTICE3:def_21; (% r) % = % r ; hence ("\/" (X,L)) % <= r by A2, LATTICE3:7; ::_thesis: verum end; X is_less_than "\/" (X,L) by LATTICE3:def_21; then A3: X is_<=_than ("\/" (X,L)) % by LATTICE3:30; then ex_sup_of X, LattPOSet L by A1, Th15; hence "\/" (X,L) = "\/" (X,(LattPOSet L)) by A3, A1, Def9; ::_thesis: "/\" (X,L) = "/\" (X,(LattPOSet L)) A4: now__::_thesis:_for_r_being_Element_of_(LattPOSet_L)_st_X_is_>=_than_r_holds_ ("/\"_(X,L))_%_>=_r let r be Element of (LattPOSet L); ::_thesis: ( X is_>=_than r implies ("/\" (X,L)) % >= r ) assume X is_>=_than r ; ::_thesis: ("/\" (X,L)) % >= r then X is_greater_than % r by LATTICE3:29; then A5: % r [= "/\" (X,L) by LATTICE3:34; (% r) % = % r ; hence ("/\" (X,L)) % >= r by A5, LATTICE3:7; ::_thesis: verum end; X is_greater_than "/\" (X,L) by LATTICE3:34; then A6: X is_>=_than ("/\" (X,L)) % by LATTICE3:28; then ex_inf_of X, LattPOSet L by A4, Th16; hence "/\" (X,L) = "/\" (X,(LattPOSet L)) by A6, A4, Def10; ::_thesis: verum end; theorem Th30: :: YELLOW_0:30 for L being antisymmetric RelStr for a being Element of L for X being set holds ( a = "\/" (X,L) & ex_sup_of X,L iff ( a is_>=_than X & ( for b being Element of L st b is_>=_than X holds a <= b ) ) ) proof let L be antisymmetric RelStr ; ::_thesis: for a being Element of L for X being set holds ( a = "\/" (X,L) & ex_sup_of X,L iff ( a is_>=_than X & ( for b being Element of L st b is_>=_than X holds a <= b ) ) ) let a be Element of L; ::_thesis: for X being set holds ( a = "\/" (X,L) & ex_sup_of X,L iff ( a is_>=_than X & ( for b being Element of L st b is_>=_than X holds a <= b ) ) ) let X be set ; ::_thesis: ( a = "\/" (X,L) & ex_sup_of X,L iff ( a is_>=_than X & ( for b being Element of L st b is_>=_than X holds a <= b ) ) ) ( a is_>=_than X & ( for b being Element of L st b is_>=_than X holds a <= b ) implies ex_sup_of X,L ) by Th15; hence ( a = "\/" (X,L) & ex_sup_of X,L iff ( a is_>=_than X & ( for b being Element of L st b is_>=_than X holds a <= b ) ) ) by Def9; ::_thesis: verum end; theorem Th31: :: YELLOW_0:31 for L being antisymmetric RelStr for a being Element of L for X being set holds ( a = "/\" (X,L) & ex_inf_of X,L iff ( a is_<=_than X & ( for b being Element of L st b is_<=_than X holds a >= b ) ) ) proof let L be antisymmetric RelStr ; ::_thesis: for a being Element of L for X being set holds ( a = "/\" (X,L) & ex_inf_of X,L iff ( a is_<=_than X & ( for b being Element of L st b is_<=_than X holds a >= b ) ) ) let a be Element of L; ::_thesis: for X being set holds ( a = "/\" (X,L) & ex_inf_of X,L iff ( a is_<=_than X & ( for b being Element of L st b is_<=_than X holds a >= b ) ) ) let X be set ; ::_thesis: ( a = "/\" (X,L) & ex_inf_of X,L iff ( a is_<=_than X & ( for b being Element of L st b is_<=_than X holds a >= b ) ) ) ( a is_<=_than X & ( for b being Element of L st b is_<=_than X holds a >= b ) implies ex_inf_of X,L ) by Th16; hence ( a = "/\" (X,L) & ex_inf_of X,L iff ( a is_<=_than X & ( for b being Element of L st b is_<=_than X holds a >= b ) ) ) by Def10; ::_thesis: verum end; theorem :: YELLOW_0:32 for L being non empty antisymmetric complete RelStr for a being Element of L for X being set holds ( a = "\/" (X,L) iff ( a is_>=_than X & ( for b being Element of L st b is_>=_than X holds a <= b ) ) ) proof let L be non empty antisymmetric complete RelStr ; ::_thesis: for a being Element of L for X being set holds ( a = "\/" (X,L) iff ( a is_>=_than X & ( for b being Element of L st b is_>=_than X holds a <= b ) ) ) let a be Element of L; ::_thesis: for X being set holds ( a = "\/" (X,L) iff ( a is_>=_than X & ( for b being Element of L st b is_>=_than X holds a <= b ) ) ) let X be set ; ::_thesis: ( a = "\/" (X,L) iff ( a is_>=_than X & ( for b being Element of L st b is_>=_than X holds a <= b ) ) ) ex_sup_of X,L by Th17; hence ( a = "\/" (X,L) iff ( a is_>=_than X & ( for b being Element of L st b is_>=_than X holds a <= b ) ) ) by Th30; ::_thesis: verum end; theorem :: YELLOW_0:33 for L being non empty antisymmetric complete RelStr for a being Element of L for X being set holds ( a = "/\" (X,L) iff ( a is_<=_than X & ( for b being Element of L st b is_<=_than X holds a >= b ) ) ) proof let L be non empty antisymmetric complete RelStr ; ::_thesis: for a being Element of L for X being set holds ( a = "/\" (X,L) iff ( a is_<=_than X & ( for b being Element of L st b is_<=_than X holds a >= b ) ) ) let a be Element of L; ::_thesis: for X being set holds ( a = "/\" (X,L) iff ( a is_<=_than X & ( for b being Element of L st b is_<=_than X holds a >= b ) ) ) let X be set ; ::_thesis: ( a = "/\" (X,L) iff ( a is_<=_than X & ( for b being Element of L st b is_<=_than X holds a >= b ) ) ) ex_inf_of X,L by Th17; hence ( a = "/\" (X,L) iff ( a is_<=_than X & ( for b being Element of L st b is_<=_than X holds a >= b ) ) ) by Th31; ::_thesis: verum end; theorem Th34: :: YELLOW_0:34 for L being RelStr for X, Y being set st X c= Y & ex_sup_of X,L & ex_sup_of Y,L holds "\/" (X,L) <= "\/" (Y,L) proof let L be RelStr ; ::_thesis: for X, Y being set st X c= Y & ex_sup_of X,L & ex_sup_of Y,L holds "\/" (X,L) <= "\/" (Y,L) let X, Y be set ; ::_thesis: ( X c= Y & ex_sup_of X,L & ex_sup_of Y,L implies "\/" (X,L) <= "\/" (Y,L) ) assume that A1: X c= Y and A2: ex_sup_of X,L and A3: ex_sup_of Y,L ; ::_thesis: "\/" (X,L) <= "\/" (Y,L) "\/" (Y,L) is_>=_than X proof let x be Element of L; :: according to LATTICE3:def_9 ::_thesis: ( not x in X or x <= "\/" (Y,L) ) assume A4: x in X ; ::_thesis: x <= "\/" (Y,L) "\/" (Y,L) is_>=_than Y by A3, Def9; hence x <= "\/" (Y,L) by A1, A4, LATTICE3:def_9; ::_thesis: verum end; hence "\/" (X,L) <= "\/" (Y,L) by A2, Def9; ::_thesis: verum end; theorem Th35: :: YELLOW_0:35 for L being RelStr for X, Y being set st X c= Y & ex_inf_of X,L & ex_inf_of Y,L holds "/\" (X,L) >= "/\" (Y,L) proof let L be RelStr ; ::_thesis: for X, Y being set st X c= Y & ex_inf_of X,L & ex_inf_of Y,L holds "/\" (X,L) >= "/\" (Y,L) let X, Y be set ; ::_thesis: ( X c= Y & ex_inf_of X,L & ex_inf_of Y,L implies "/\" (X,L) >= "/\" (Y,L) ) assume that A1: X c= Y and A2: ex_inf_of X,L and A3: ex_inf_of Y,L ; ::_thesis: "/\" (X,L) >= "/\" (Y,L) "/\" (Y,L) is_<=_than X proof let x be Element of L; :: according to LATTICE3:def_8 ::_thesis: ( not x in X or "/\" (Y,L) <= x ) assume A4: x in X ; ::_thesis: "/\" (Y,L) <= x "/\" (Y,L) is_<=_than Y by A3, Def10; hence "/\" (Y,L) <= x by A1, A4, LATTICE3:def_8; ::_thesis: verum end; hence "/\" (X,L) >= "/\" (Y,L) by A2, Def10; ::_thesis: verum end; theorem :: YELLOW_0:36 for L being transitive antisymmetric RelStr for X, Y being set st ex_sup_of X,L & ex_sup_of Y,L & ex_sup_of X \/ Y,L holds "\/" ((X \/ Y),L) = ("\/" (X,L)) "\/" ("\/" (Y,L)) proof let L be transitive antisymmetric RelStr ; ::_thesis: for X, Y being set st ex_sup_of X,L & ex_sup_of Y,L & ex_sup_of X \/ Y,L holds "\/" ((X \/ Y),L) = ("\/" (X,L)) "\/" ("\/" (Y,L)) let X, Y be set ; ::_thesis: ( ex_sup_of X,L & ex_sup_of Y,L & ex_sup_of X \/ Y,L implies "\/" ((X \/ Y),L) = ("\/" (X,L)) "\/" ("\/" (Y,L)) ) assume that A1: ( ex_sup_of X,L & ex_sup_of Y,L ) and A2: ex_sup_of X \/ Y,L ; ::_thesis: "\/" ((X \/ Y),L) = ("\/" (X,L)) "\/" ("\/" (Y,L)) set a = "\/" (X,L); set b = "\/" (Y,L); set c = "\/" ((X \/ Y),L); A3: ( "\/" (X,L) is_>=_than X & "\/" (Y,L) is_>=_than Y ) by A1, Th30; A4: now__::_thesis:_for_d_being_Element_of_L_st_d_>=_"\/"_(X,L)_&_d_>=_"\/"_(Y,L)_holds_ "\/"_((X_\/_Y),L)_<=_d let d be Element of L; ::_thesis: ( d >= "\/" (X,L) & d >= "\/" (Y,L) implies "\/" ((X \/ Y),L) <= d ) assume ( d >= "\/" (X,L) & d >= "\/" (Y,L) ) ; ::_thesis: "\/" ((X \/ Y),L) <= d then ( d is_>=_than X & d is_>=_than Y ) by A3, Th4; then d is_>=_than X \/ Y by Th10; hence "\/" ((X \/ Y),L) <= d by A2, Th30; ::_thesis: verum end; ( "\/" ((X \/ Y),L) >= "\/" (X,L) & "\/" ((X \/ Y),L) >= "\/" (Y,L) ) by A1, A2, Th34, XBOOLE_1:7; hence "\/" ((X \/ Y),L) = ("\/" (X,L)) "\/" ("\/" (Y,L)) by A4, Th18; ::_thesis: verum end; theorem :: YELLOW_0:37 for L being transitive antisymmetric RelStr for X, Y being set st ex_inf_of X,L & ex_inf_of Y,L & ex_inf_of X \/ Y,L holds "/\" ((X \/ Y),L) = ("/\" (X,L)) "/\" ("/\" (Y,L)) proof let L be transitive antisymmetric RelStr ; ::_thesis: for X, Y being set st ex_inf_of X,L & ex_inf_of Y,L & ex_inf_of X \/ Y,L holds "/\" ((X \/ Y),L) = ("/\" (X,L)) "/\" ("/\" (Y,L)) let X, Y be set ; ::_thesis: ( ex_inf_of X,L & ex_inf_of Y,L & ex_inf_of X \/ Y,L implies "/\" ((X \/ Y),L) = ("/\" (X,L)) "/\" ("/\" (Y,L)) ) assume that A1: ( ex_inf_of X,L & ex_inf_of Y,L ) and A2: ex_inf_of X \/ Y,L ; ::_thesis: "/\" ((X \/ Y),L) = ("/\" (X,L)) "/\" ("/\" (Y,L)) set a = "/\" (X,L); set b = "/\" (Y,L); set c = "/\" ((X \/ Y),L); A3: ( "/\" (X,L) is_<=_than X & "/\" (Y,L) is_<=_than Y ) by A1, Th31; A4: now__::_thesis:_for_d_being_Element_of_L_st_d_<=_"/\"_(X,L)_&_d_<=_"/\"_(Y,L)_holds_ "/\"_((X_\/_Y),L)_>=_d let d be Element of L; ::_thesis: ( d <= "/\" (X,L) & d <= "/\" (Y,L) implies "/\" ((X \/ Y),L) >= d ) assume ( d <= "/\" (X,L) & d <= "/\" (Y,L) ) ; ::_thesis: "/\" ((X \/ Y),L) >= d then ( d is_<=_than X & d is_<=_than Y ) by A3, Th4; then d is_<=_than X \/ Y by Th10; hence "/\" ((X \/ Y),L) >= d by A2, Th31; ::_thesis: verum end; ( "/\" ((X \/ Y),L) <= "/\" (X,L) & "/\" ((X \/ Y),L) <= "/\" (Y,L) ) by A1, A2, Th35, XBOOLE_1:7; hence "/\" ((X \/ Y),L) = ("/\" (X,L)) "/\" ("/\" (Y,L)) by A4, Th19; ::_thesis: verum end; notation let L be RelStr ; let X be Subset of L; synonym sup X for "\/" (X,L); synonym inf X for "/\" (X,L); end; theorem Th38: :: YELLOW_0:38 for L being non empty reflexive antisymmetric RelStr for a being Element of L holds ( ex_sup_of {a},L & ex_inf_of {a},L ) proof let L be non empty reflexive antisymmetric RelStr ; ::_thesis: for a being Element of L holds ( ex_sup_of {a},L & ex_inf_of {a},L ) let a be Element of L; ::_thesis: ( ex_sup_of {a},L & ex_inf_of {a},L ) A1: for b being Element of L st b is_>=_than {a} holds b >= a by Th7; A2: a <= a ; then a is_>=_than {a} by Th7; hence ex_sup_of {a},L by A1, Th15; ::_thesis: ex_inf_of {a},L A3: for b being Element of L st b is_<=_than {a} holds b <= a by Th7; a is_<=_than {a} by A2, Th7; hence ex_inf_of {a},L by A3, Th16; ::_thesis: verum end; theorem :: YELLOW_0:39 for L being non empty reflexive antisymmetric RelStr for a being Element of L holds ( sup {a} = a & inf {a} = a ) proof let L be non empty reflexive antisymmetric RelStr ; ::_thesis: for a being Element of L holds ( sup {a} = a & inf {a} = a ) let a be Element of L; ::_thesis: ( sup {a} = a & inf {a} = a ) A1: for b being Element of L st b is_>=_than {a} holds b >= a by Th7; A2: a <= a ; then a is_>=_than {a} by Th7; hence sup {a} = a by A1, Th30; ::_thesis: inf {a} = a A3: for b being Element of L st b is_<=_than {a} holds b <= a by Th7; a is_<=_than {a} by A2, Th7; hence inf {a} = a by A3, Th31; ::_thesis: verum end; theorem Th40: :: YELLOW_0:40 for L being with_infima Poset for a, b being Element of L holds inf {a,b} = a "/\" b proof let L be with_infima Poset; ::_thesis: for a, b being Element of L holds inf {a,b} = a "/\" b let a, b be Element of L; ::_thesis: inf {a,b} = a "/\" b A1: now__::_thesis:_for_c_being_Element_of_L_st_c_is_<=_than_{a,b}_holds_ c_<=_a_"/\"_b let c be Element of L; ::_thesis: ( c is_<=_than {a,b} implies c <= a "/\" b ) assume c is_<=_than {a,b} ; ::_thesis: c <= a "/\" b then ( c <= a & c <= b ) by Th8; hence c <= a "/\" b by Th23; ::_thesis: verum end; ( a "/\" b <= a & a "/\" b <= b ) by Th23; then A2: a "/\" b is_<=_than {a,b} by Th8; then ex_inf_of {a,b},L by A1, Th16; hence inf {a,b} = a "/\" b by A2, A1, Def10; ::_thesis: verum end; theorem Th41: :: YELLOW_0:41 for L being with_suprema Poset for a, b being Element of L holds sup {a,b} = a "\/" b proof let L be with_suprema Poset; ::_thesis: for a, b being Element of L holds sup {a,b} = a "\/" b let a, b be Element of L; ::_thesis: sup {a,b} = a "\/" b A1: now__::_thesis:_for_c_being_Element_of_L_st_c_is_>=_than_{a,b}_holds_ c_>=_a_"\/"_b let c be Element of L; ::_thesis: ( c is_>=_than {a,b} implies c >= a "\/" b ) assume c is_>=_than {a,b} ; ::_thesis: c >= a "\/" b then ( c >= a & c >= b ) by Th8; hence c >= a "\/" b by Th22; ::_thesis: verum end; ( a "\/" b >= a & a "\/" b >= b ) by Th22; then A2: a "\/" b is_>=_than {a,b} by Th8; then ex_sup_of {a,b},L by A1, Th15; hence sup {a,b} = a "\/" b by A2, A1, Def9; ::_thesis: verum end; theorem Th42: :: YELLOW_0:42 for L being non empty antisymmetric lower-bounded RelStr holds ( ex_sup_of {} ,L & ex_inf_of the carrier of L,L ) proof let L be non empty antisymmetric lower-bounded RelStr ; ::_thesis: ( ex_sup_of {} ,L & ex_inf_of the carrier of L,L ) consider a being Element of L such that A1: a is_<=_than the carrier of L by Def4; now__::_thesis:_ex_a_being_Element_of_L_st_ (_a_is_>=_than_{}_&_(_for_b_being_Element_of_L_st_b_is_>=_than_{}_holds_ a_<=_b_)_) take a = a; ::_thesis: ( a is_>=_than {} & ( for b being Element of L st b is_>=_than {} holds a <= b ) ) thus a is_>=_than {} by Th6; ::_thesis: for b being Element of L st b is_>=_than {} holds a <= b thus for b being Element of L st b is_>=_than {} holds a <= b by A1, LATTICE3:def_8; ::_thesis: verum end; hence ex_sup_of {} ,L by Th15; ::_thesis: ex_inf_of the carrier of L,L for b being Element of L st the carrier of L is_>=_than b holds a >= b by LATTICE3:def_8; hence ex_inf_of the carrier of L,L by A1, Th16; ::_thesis: verum end; theorem Th43: :: YELLOW_0:43 for L being non empty antisymmetric upper-bounded RelStr holds ( ex_inf_of {} ,L & ex_sup_of the carrier of L,L ) proof let L be non empty antisymmetric upper-bounded RelStr ; ::_thesis: ( ex_inf_of {} ,L & ex_sup_of the carrier of L,L ) consider a being Element of L such that A1: a is_>=_than the carrier of L by Def5; now__::_thesis:_ex_a_being_Element_of_L_st_ (_a_is_<=_than_{}_&_(_for_b_being_Element_of_L_st_b_is_<=_than_{}_holds_ a_>=_b_)_) take a = a; ::_thesis: ( a is_<=_than {} & ( for b being Element of L st b is_<=_than {} holds a >= b ) ) thus a is_<=_than {} by Th6; ::_thesis: for b being Element of L st b is_<=_than {} holds a >= b thus for b being Element of L st b is_<=_than {} holds a >= b by A1, LATTICE3:def_9; ::_thesis: verum end; hence ex_inf_of {} ,L by Th16; ::_thesis: ex_sup_of the carrier of L,L for b being Element of L st the carrier of L is_<=_than b holds a <= b by LATTICE3:def_9; hence ex_sup_of the carrier of L,L by A1, Th15; ::_thesis: verum end; definition let L be RelStr ; func Bottom L -> Element of L equals :: YELLOW_0:def 11 "\/" ({},L); correctness coherence "\/" ({},L) is Element of L; ; func Top L -> Element of L equals :: YELLOW_0:def 12 "/\" ({},L); correctness coherence "/\" ({},L) is Element of L; ; end; :: deftheorem defines Bottom YELLOW_0:def_11_:_ for L being RelStr holds Bottom L = "\/" ({},L); :: deftheorem defines Top YELLOW_0:def_12_:_ for L being RelStr holds Top L = "/\" ({},L); theorem :: YELLOW_0:44 for L being non empty antisymmetric lower-bounded RelStr for x being Element of L holds Bottom L <= x proof let L be non empty antisymmetric lower-bounded RelStr ; ::_thesis: for x being Element of L holds Bottom L <= x let x be Element of L; ::_thesis: Bottom L <= x ( {} is_<=_than x & ex_sup_of {} ,L ) by Th6, Th42; hence Bottom L <= x by Th30; ::_thesis: verum end; theorem :: YELLOW_0:45 for L being non empty antisymmetric upper-bounded RelStr for x being Element of L holds x <= Top L proof let L be non empty antisymmetric upper-bounded RelStr ; ::_thesis: for x being Element of L holds x <= Top L let x be Element of L; ::_thesis: x <= Top L ( {} is_>=_than x & ex_inf_of {} ,L ) by Th6, Th43; hence x <= Top L by Th31; ::_thesis: verum end; theorem Th46: :: YELLOW_0:46 for L being non empty RelStr for X, Y being set st ( for x being Element of L holds ( x is_>=_than X iff x is_>=_than Y ) ) & ex_sup_of X,L holds ex_sup_of Y,L proof let L be non empty RelStr ; ::_thesis: for X, Y being set st ( for x being Element of L holds ( x is_>=_than X iff x is_>=_than Y ) ) & ex_sup_of X,L holds ex_sup_of Y,L let X, Y be set ; ::_thesis: ( ( for x being Element of L holds ( x is_>=_than X iff x is_>=_than Y ) ) & ex_sup_of X,L implies ex_sup_of Y,L ) assume A1: for x being Element of L holds ( x is_>=_than X iff x is_>=_than Y ) ; ::_thesis: ( not ex_sup_of X,L or ex_sup_of Y,L ) given a being Element of L such that A2: X is_<=_than a and A3: for b being Element of L st X is_<=_than b holds a <= b and A4: for c being Element of L st X is_<=_than c & ( for b being Element of L st X is_<=_than b holds c <= b ) holds c = a ; :: according to YELLOW_0:def_7 ::_thesis: ex_sup_of Y,L take a ; :: according to YELLOW_0:def_7 ::_thesis: ( Y is_<=_than a & ( for b being Element of L st Y is_<=_than b holds b >= a ) & ( for c being Element of L st Y is_<=_than c & ( for b being Element of L st Y is_<=_than b holds b >= c ) holds c = a ) ) thus Y is_<=_than a by A1, A2; ::_thesis: ( ( for b being Element of L st Y is_<=_than b holds b >= a ) & ( for c being Element of L st Y is_<=_than c & ( for b being Element of L st Y is_<=_than b holds b >= c ) holds c = a ) ) hereby ::_thesis: for c being Element of L st Y is_<=_than c & ( for b being Element of L st Y is_<=_than b holds b >= c ) holds c = a let b be Element of L; ::_thesis: ( Y is_<=_than b implies a <= b ) assume Y is_<=_than b ; ::_thesis: a <= b then X is_<=_than b by A1; hence a <= b by A3; ::_thesis: verum end; let c be Element of L; ::_thesis: ( Y is_<=_than c & ( for b being Element of L st Y is_<=_than b holds b >= c ) implies c = a ) assume A5: Y is_<=_than c ; ::_thesis: ( ex b being Element of L st ( Y is_<=_than b & not b >= c ) or c = a ) assume A6: for b being Element of L st Y is_<=_than b holds c <= b ; ::_thesis: c = a A7: now__::_thesis:_for_b_being_Element_of_L_st_X_is_<=_than_b_holds_ c_<=_b let b be Element of L; ::_thesis: ( X is_<=_than b implies c <= b ) assume X is_<=_than b ; ::_thesis: c <= b then Y is_<=_than b by A1; hence c <= b by A6; ::_thesis: verum end; X is_<=_than c by A1, A5; hence c = a by A4, A7; ::_thesis: verum end; theorem Th47: :: YELLOW_0:47 for L being non empty RelStr for X, Y being set st ex_sup_of X,L & ( for x being Element of L holds ( x is_>=_than X iff x is_>=_than Y ) ) holds "\/" (X,L) = "\/" (Y,L) proof let L be non empty RelStr ; ::_thesis: for X, Y being set st ex_sup_of X,L & ( for x being Element of L holds ( x is_>=_than X iff x is_>=_than Y ) ) holds "\/" (X,L) = "\/" (Y,L) let X, Y be set ; ::_thesis: ( ex_sup_of X,L & ( for x being Element of L holds ( x is_>=_than X iff x is_>=_than Y ) ) implies "\/" (X,L) = "\/" (Y,L) ) assume A1: ex_sup_of X,L ; ::_thesis: ( ex x being Element of L st ( ( x is_>=_than X implies x is_>=_than Y ) implies ( x is_>=_than Y & not x is_>=_than X ) ) or "\/" (X,L) = "\/" (Y,L) ) assume A2: for x being Element of L holds ( x is_>=_than X iff x is_>=_than Y ) ; ::_thesis: "\/" (X,L) = "\/" (Y,L) A3: now__::_thesis:_for_b_being_Element_of_L_st_Y_is_<=_than_b_holds_ "\/"_(X,L)_<=_b let b be Element of L; ::_thesis: ( Y is_<=_than b implies "\/" (X,L) <= b ) assume Y is_<=_than b ; ::_thesis: "\/" (X,L) <= b then X is_<=_than b by A2; hence "\/" (X,L) <= b by A1, Def9; ::_thesis: verum end; X is_<=_than "\/" (X,L) by A1, Def9; then A4: Y is_<=_than "\/" (X,L) by A2; ex_sup_of Y,L by A1, A2, Th46; hence "\/" (X,L) = "\/" (Y,L) by A4, A3, Def9; ::_thesis: verum end; theorem Th48: :: YELLOW_0:48 for L being non empty RelStr for X, Y being set st ( for x being Element of L holds ( x is_<=_than X iff x is_<=_than Y ) ) & ex_inf_of X,L holds ex_inf_of Y,L proof let L be non empty RelStr ; ::_thesis: for X, Y being set st ( for x being Element of L holds ( x is_<=_than X iff x is_<=_than Y ) ) & ex_inf_of X,L holds ex_inf_of Y,L let X, Y be set ; ::_thesis: ( ( for x being Element of L holds ( x is_<=_than X iff x is_<=_than Y ) ) & ex_inf_of X,L implies ex_inf_of Y,L ) assume A1: for x being Element of L holds ( x is_<=_than X iff x is_<=_than Y ) ; ::_thesis: ( not ex_inf_of X,L or ex_inf_of Y,L ) given a being Element of L such that A2: X is_>=_than a and A3: for b being Element of L st X is_>=_than b holds a >= b and A4: for c being Element of L st X is_>=_than c & ( for b being Element of L st X is_>=_than b holds c >= b ) holds c = a ; :: according to YELLOW_0:def_8 ::_thesis: ex_inf_of Y,L take a ; :: according to YELLOW_0:def_8 ::_thesis: ( Y is_>=_than a & ( for b being Element of L st Y is_>=_than b holds b <= a ) & ( for c being Element of L st Y is_>=_than c & ( for b being Element of L st Y is_>=_than b holds b <= c ) holds c = a ) ) thus Y is_>=_than a by A1, A2; ::_thesis: ( ( for b being Element of L st Y is_>=_than b holds b <= a ) & ( for c being Element of L st Y is_>=_than c & ( for b being Element of L st Y is_>=_than b holds b <= c ) holds c = a ) ) hereby ::_thesis: for c being Element of L st Y is_>=_than c & ( for b being Element of L st Y is_>=_than b holds b <= c ) holds c = a let b be Element of L; ::_thesis: ( Y is_>=_than b implies a >= b ) assume Y is_>=_than b ; ::_thesis: a >= b then X is_>=_than b by A1; hence a >= b by A3; ::_thesis: verum end; let c be Element of L; ::_thesis: ( Y is_>=_than c & ( for b being Element of L st Y is_>=_than b holds b <= c ) implies c = a ) assume A5: Y is_>=_than c ; ::_thesis: ( ex b being Element of L st ( Y is_>=_than b & not b <= c ) or c = a ) assume A6: for b being Element of L st Y is_>=_than b holds c >= b ; ::_thesis: c = a A7: now__::_thesis:_for_b_being_Element_of_L_st_X_is_>=_than_b_holds_ c_>=_b let b be Element of L; ::_thesis: ( X is_>=_than b implies c >= b ) assume X is_>=_than b ; ::_thesis: c >= b then Y is_>=_than b by A1; hence c >= b by A6; ::_thesis: verum end; X is_>=_than c by A1, A5; hence c = a by A4, A7; ::_thesis: verum end; theorem Th49: :: YELLOW_0:49 for L being non empty RelStr for X, Y being set st ex_inf_of X,L & ( for x being Element of L holds ( x is_<=_than X iff x is_<=_than Y ) ) holds "/\" (X,L) = "/\" (Y,L) proof let L be non empty RelStr ; ::_thesis: for X, Y being set st ex_inf_of X,L & ( for x being Element of L holds ( x is_<=_than X iff x is_<=_than Y ) ) holds "/\" (X,L) = "/\" (Y,L) let X, Y be set ; ::_thesis: ( ex_inf_of X,L & ( for x being Element of L holds ( x is_<=_than X iff x is_<=_than Y ) ) implies "/\" (X,L) = "/\" (Y,L) ) assume A1: ex_inf_of X,L ; ::_thesis: ( ex x being Element of L st ( ( x is_<=_than X implies x is_<=_than Y ) implies ( x is_<=_than Y & not x is_<=_than X ) ) or "/\" (X,L) = "/\" (Y,L) ) assume A2: for x being Element of L holds ( x is_<=_than X iff x is_<=_than Y ) ; ::_thesis: "/\" (X,L) = "/\" (Y,L) A3: now__::_thesis:_for_b_being_Element_of_L_st_Y_is_>=_than_b_holds_ "/\"_(X,L)_>=_b let b be Element of L; ::_thesis: ( Y is_>=_than b implies "/\" (X,L) >= b ) assume Y is_>=_than b ; ::_thesis: "/\" (X,L) >= b then X is_>=_than b by A2; hence "/\" (X,L) >= b by A1, Def10; ::_thesis: verum end; X is_>=_than "/\" (X,L) by A1, Def10; then A4: Y is_>=_than "/\" (X,L) by A2; ex_inf_of Y,L by A1, A2, Th48; hence "/\" (X,L) = "/\" (Y,L) by A4, A3, Def10; ::_thesis: verum end; theorem Th50: :: YELLOW_0:50 for L being non empty RelStr for X being set holds ( ( ex_sup_of X,L implies ex_sup_of X /\ the carrier of L,L ) & ( ex_sup_of X /\ the carrier of L,L implies ex_sup_of X,L ) & ( ex_inf_of X,L implies ex_inf_of X /\ the carrier of L,L ) & ( ex_inf_of X /\ the carrier of L,L implies ex_inf_of X,L ) ) proof let L be non empty RelStr ; ::_thesis: for X being set holds ( ( ex_sup_of X,L implies ex_sup_of X /\ the carrier of L,L ) & ( ex_sup_of X /\ the carrier of L,L implies ex_sup_of X,L ) & ( ex_inf_of X,L implies ex_inf_of X /\ the carrier of L,L ) & ( ex_inf_of X /\ the carrier of L,L implies ex_inf_of X,L ) ) let X be set ; ::_thesis: ( ( ex_sup_of X,L implies ex_sup_of X /\ the carrier of L,L ) & ( ex_sup_of X /\ the carrier of L,L implies ex_sup_of X,L ) & ( ex_inf_of X,L implies ex_inf_of X /\ the carrier of L,L ) & ( ex_inf_of X /\ the carrier of L,L implies ex_inf_of X,L ) ) set Y = X /\ the carrier of L; ( ( for x being Element of L holds ( x is_<=_than X iff x is_<=_than X /\ the carrier of L ) ) & ( for x being Element of L holds ( x is_>=_than X iff x is_>=_than X /\ the carrier of L ) ) ) by Th5; hence ( ( ex_sup_of X,L implies ex_sup_of X /\ the carrier of L,L ) & ( ex_sup_of X /\ the carrier of L,L implies ex_sup_of X,L ) & ( ex_inf_of X,L implies ex_inf_of X /\ the carrier of L,L ) & ( ex_inf_of X /\ the carrier of L,L implies ex_inf_of X,L ) ) by Th46, Th48; ::_thesis: verum end; theorem :: YELLOW_0:51 for L being non empty RelStr for X being set st ( ex_sup_of X,L or ex_sup_of X /\ the carrier of L,L ) holds "\/" (X,L) = "\/" ((X /\ the carrier of L),L) proof let L be non empty RelStr ; ::_thesis: for X being set st ( ex_sup_of X,L or ex_sup_of X /\ the carrier of L,L ) holds "\/" (X,L) = "\/" ((X /\ the carrier of L),L) let X be set ; ::_thesis: ( ( ex_sup_of X,L or ex_sup_of X /\ the carrier of L,L ) implies "\/" (X,L) = "\/" ((X /\ the carrier of L),L) ) set Y = X /\ the carrier of L; assume A1: ( ex_sup_of X,L or ex_sup_of X /\ the carrier of L,L ) ; ::_thesis: "\/" (X,L) = "\/" ((X /\ the carrier of L),L) for x being Element of L holds ( x is_>=_than X iff x is_>=_than X /\ the carrier of L ) by Th5; hence "\/" (X,L) = "\/" ((X /\ the carrier of L),L) by A1, Th47; ::_thesis: verum end; theorem :: YELLOW_0:52 for L being non empty RelStr for X being set st ( ex_inf_of X,L or ex_inf_of X /\ the carrier of L,L ) holds "/\" (X,L) = "/\" ((X /\ the carrier of L),L) proof let L be non empty RelStr ; ::_thesis: for X being set st ( ex_inf_of X,L or ex_inf_of X /\ the carrier of L,L ) holds "/\" (X,L) = "/\" ((X /\ the carrier of L),L) let X be set ; ::_thesis: ( ( ex_inf_of X,L or ex_inf_of X /\ the carrier of L,L ) implies "/\" (X,L) = "/\" ((X /\ the carrier of L),L) ) set Y = X /\ the carrier of L; assume A1: ( ex_inf_of X,L or ex_inf_of X /\ the carrier of L,L ) ; ::_thesis: "/\" (X,L) = "/\" ((X /\ the carrier of L),L) for x being Element of L holds ( x is_<=_than X iff x is_<=_than X /\ the carrier of L ) by Th5; hence "/\" (X,L) = "/\" ((X /\ the carrier of L),L) by A1, Th49; ::_thesis: verum end; theorem :: YELLOW_0:53 for L being non empty RelStr st ( for X being Subset of L holds ex_sup_of X,L ) holds L is complete proof let L be non empty RelStr ; ::_thesis: ( ( for X being Subset of L holds ex_sup_of X,L ) implies L is complete ) assume A1: for X being Subset of L holds ex_sup_of X,L ; ::_thesis: L is complete let X be set ; :: according to LATTICE3:def_12 ::_thesis: ex b1 being Element of the carrier of L st ( X is_<=_than b1 & ( for b2 being Element of the carrier of L holds ( not X is_<=_than b2 or b1 <= b2 ) ) ) take "\/" (X,L) ; ::_thesis: ( X is_<=_than "\/" (X,L) & ( for b1 being Element of the carrier of L holds ( not X is_<=_than b1 or "\/" (X,L) <= b1 ) ) ) reconsider Y = X /\ the carrier of L as Subset of L by XBOOLE_1:17; ex_sup_of Y,L by A1; then ex_sup_of X,L by Th50; hence ( X is_<=_than "\/" (X,L) & ( for b1 being Element of the carrier of L holds ( not X is_<=_than b1 or "\/" (X,L) <= b1 ) ) ) by Def9; ::_thesis: verum end; theorem :: YELLOW_0:54 for L being non empty Poset holds ( L is with_suprema iff for X being non empty finite Subset of L holds ex_sup_of X,L ) proof let L be non empty Poset; ::_thesis: ( L is with_suprema iff for X being non empty finite Subset of L holds ex_sup_of X,L ) hereby ::_thesis: ( ( for X being non empty finite Subset of L holds ex_sup_of X,L ) implies L is with_suprema ) defpred S1[ set ] means ( not \$1 is empty implies ex_sup_of \$1,L ); assume A1: L is with_suprema ; ::_thesis: for X being non empty finite Subset of L holds ex_sup_of X,L let X be non empty finite Subset of L; ::_thesis: ex_sup_of X,L A2: for x, Y being set st x in X & Y c= X & S1[Y] holds S1[Y \/ {x}] proof let x, Y be set ; ::_thesis: ( x in X & Y c= X & S1[Y] implies S1[Y \/ {x}] ) assume that A3: x in X and Y c= X and A4: ( not Y is empty implies ex_sup_of Y,L ) ; ::_thesis: S1[Y \/ {x}] reconsider z = x as Element of L by A3; assume not Y \/ {x} is empty ; ::_thesis: ex_sup_of Y \/ {x},L percases ( Y is empty or not Y is empty ) ; suppose Y is empty ; ::_thesis: ex_sup_of Y \/ {x},L then Y \/ {x} = {z} ; hence ex_sup_of Y \/ {x},L by Th38; ::_thesis: verum end; supposeA5: not Y is empty ; ::_thesis: ex_sup_of Y \/ {x},L thus ex_sup_of Y \/ {x},L ::_thesis: verum proof take a = ("\/" (Y,L)) "\/" z; :: according to YELLOW_0:def_7 ::_thesis: ( Y \/ {x} is_<=_than a & ( for b being Element of L st Y \/ {x} is_<=_than b holds b >= a ) & ( for c being Element of L st Y \/ {x} is_<=_than c & ( for b being Element of L st Y \/ {x} is_<=_than b holds b >= c ) holds c = a ) ) A6: Y is_<=_than "\/" (Y,L) by A4, A5, Def9; A7: ex_sup_of {("\/" (Y,L)),z},L by A1, Th20; then z <= a by Th18; then A8: {x} is_<=_than a by Th7; "\/" (Y,L) <= a by A7, Th18; then A9: Y is_<=_than a by A6, Th11; hence Y \/ {x} is_<=_than a by A8, Th10; ::_thesis: ( ( for b being Element of L st Y \/ {x} is_<=_than b holds b >= a ) & ( for c being Element of L st Y \/ {x} is_<=_than c & ( for b being Element of L st Y \/ {x} is_<=_than b holds b >= c ) holds c = a ) ) hereby ::_thesis: for c being Element of L st Y \/ {x} is_<=_than c & ( for b being Element of L st Y \/ {x} is_<=_than b holds b >= c ) holds c = a let b be Element of L; ::_thesis: ( Y \/ {x} is_<=_than b implies b >= a ) assume A10: Y \/ {x} is_<=_than b ; ::_thesis: b >= a Y c= Y \/ {x} by XBOOLE_1:7; then Y is_<=_than b by A10, Th9; then A11: "\/" (Y,L) <= b by A4, A5, Def9; z in {x} by TARSKI:def_1; then z in Y \/ {x} by XBOOLE_0:def_3; then z <= b by A10, LATTICE3:def_9; hence b >= a by A7, A11, Th18; ::_thesis: verum end; let c be Element of L; ::_thesis: ( Y \/ {x} is_<=_than c & ( for b being Element of L st Y \/ {x} is_<=_than b holds b >= c ) implies c = a ) assume that A12: Y \/ {x} is_<=_than c and A13: for b being Element of L st Y \/ {x} is_<=_than b holds b >= c ; ::_thesis: c = a Y c= Y \/ {x} by XBOOLE_1:7; then Y is_<=_than c by A12, Th9; then A14: "\/" (Y,L) <= c by A4, A5, Def9; z in {x} by TARSKI:def_1; then z in Y \/ {x} by XBOOLE_0:def_3; then z <= c by A12, LATTICE3:def_9; then A15: c >= a by A7, A14, Th18; a >= c by A9, A8, A13, Th10; hence c = a by A15, ORDERS_2:2; ::_thesis: verum end; end; end; end; A16: S1[ {} ] ; A17: X is finite ; S1[X] from FINSET_1:sch_2(A17, A16, A2); hence ex_sup_of X,L ; ::_thesis: verum end; assume for X being non empty finite Subset of L holds ex_sup_of X,L ; ::_thesis: L is with_suprema then for a, b being Element of L holds ex_sup_of {a,b},L ; hence L is with_suprema by Th20; ::_thesis: verum end; theorem :: YELLOW_0:55 for L being non empty Poset holds ( L is with_infima iff for X being non empty finite Subset of L holds ex_inf_of X,L ) proof let L be non empty Poset; ::_thesis: ( L is with_infima iff for X being non empty finite Subset of L holds ex_inf_of X,L ) hereby ::_thesis: ( ( for X being non empty finite Subset of L holds ex_inf_of X,L ) implies L is with_infima ) defpred S1[ set ] means ( not \$1 is empty implies ex_inf_of \$1,L ); assume A1: L is with_infima ; ::_thesis: for X being non empty finite Subset of L holds ex_inf_of X,L let X be non empty finite Subset of L; ::_thesis: ex_inf_of X,L A2: for x, Y being set st x in X & Y c= X & S1[Y] holds S1[Y \/ {x}] proof let x, Y be set ; ::_thesis: ( x in X & Y c= X & S1[Y] implies S1[Y \/ {x}] ) assume that A3: x in X and Y c= X and A4: ( not Y is empty implies ex_inf_of Y,L ) ; ::_thesis: S1[Y \/ {x}] reconsider z = x as Element of L by A3; assume not Y \/ {x} is empty ; ::_thesis: ex_inf_of Y \/ {x},L percases ( Y is empty or not Y is empty ) ; suppose Y is empty ; ::_thesis: ex_inf_of Y \/ {x},L then Y \/ {x} = {z} ; hence ex_inf_of Y \/ {x},L by Th38; ::_thesis: verum end; supposeA5: not Y is empty ; ::_thesis: ex_inf_of Y \/ {x},L thus ex_inf_of Y \/ {x},L ::_thesis: verum proof take a = ("/\" (Y,L)) "/\" z; :: according to YELLOW_0:def_8 ::_thesis: ( Y \/ {x} is_>=_than a & ( for b being Element of L st Y \/ {x} is_>=_than b holds b <= a ) & ( for c being Element of L st Y \/ {x} is_>=_than c & ( for b being Element of L st Y \/ {x} is_>=_than b holds b <= c ) holds c = a ) ) A6: Y is_>=_than "/\" (Y,L) by A4, A5, Def10; A7: ex_inf_of {("/\" (Y,L)),z},L by A1, Th21; then z >= a by Th19; then A8: {x} is_>=_than a by Th7; "/\" (Y,L) >= a by A7, Th19; then A9: Y is_>=_than a by A6, Th12; hence Y \/ {x} is_>=_than a by A8, Th10; ::_thesis: ( ( for b being Element of L st Y \/ {x} is_>=_than b holds b <= a ) & ( for c being Element of L st Y \/ {x} is_>=_than c & ( for b being Element of L st Y \/ {x} is_>=_than b holds b <= c ) holds c = a ) ) hereby ::_thesis: for c being Element of L st Y \/ {x} is_>=_than c & ( for b being Element of L st Y \/ {x} is_>=_than b holds b <= c ) holds c = a let b be Element of L; ::_thesis: ( Y \/ {x} is_>=_than b implies b <= a ) assume A10: Y \/ {x} is_>=_than b ; ::_thesis: b <= a Y c= Y \/ {x} by XBOOLE_1:7; then Y is_>=_than b by A10, Th9; then A11: "/\" (Y,L) >= b by A4, A5, Def10; z in {x} by TARSKI:def_1; then z in Y \/ {x} by XBOOLE_0:def_3; then z >= b by A10, LATTICE3:def_8; hence b <= a by A7, A11, Th19; ::_thesis: verum end; let c be Element of L; ::_thesis: ( Y \/ {x} is_>=_than c & ( for b being Element of L st Y \/ {x} is_>=_than b holds b <= c ) implies c = a ) assume that A12: Y \/ {x} is_>=_than c and A13: for b being Element of L st Y \/ {x} is_>=_than b holds b <= c ; ::_thesis: c = a Y c= Y \/ {x} by XBOOLE_1:7; then Y is_>=_than c by A12, Th9; then A14: "/\" (Y,L) >= c by A4, A5, Def10; z in {x} by TARSKI:def_1; then z in Y \/ {x} by XBOOLE_0:def_3; then z >= c by A12, LATTICE3:def_8; then A15: c <= a by A7, A14, Th19; a <= c by A9, A8, A13, Th10; hence c = a by A15, ORDERS_2:2; ::_thesis: verum end; end; end; end; A16: S1[ {} ] ; A17: X is finite ; S1[X] from FINSET_1:sch_2(A17, A16, A2); hence ex_inf_of X,L ; ::_thesis: verum end; assume for X being non empty finite Subset of L holds ex_inf_of X,L ; ::_thesis: L is with_infima then for a, b being Element of L holds ex_inf_of {a,b},L ; hence L is with_infima by Th21; ::_thesis: verum end; begin definition let L be RelStr ; mode SubRelStr of L -> RelStr means :Def13: :: YELLOW_0:def 13 ( the carrier of it c= the carrier of L & the InternalRel of it c= the InternalRel of L ); existence ex b1 being RelStr st ( the carrier of b1 c= the carrier of L & the InternalRel of b1 c= the InternalRel of L ) ; end; :: deftheorem Def13 defines SubRelStr YELLOW_0:def_13_:_ for L, b2 being RelStr holds ( b2 is SubRelStr of L iff ( the carrier of b2 c= the carrier of L & the InternalRel of b2 c= the InternalRel of L ) ); definition let L be RelStr ; let S be SubRelStr of L; attrS is full means :Def14: :: YELLOW_0:def 14 the InternalRel of S = the InternalRel of L |_2 the carrier of S; end; :: deftheorem Def14 defines full YELLOW_0:def_14_:_ for L being RelStr for S being SubRelStr of L holds ( S is full iff the InternalRel of S = the InternalRel of L |_2 the carrier of S ); registration let L be RelStr ; cluster strict full for SubRelStr of L; existence ex b1 being SubRelStr of L st ( b1 is strict & b1 is full ) proof set S = RelStr(# the carrier of L, the InternalRel of L #); reconsider S = RelStr(# the carrier of L, the InternalRel of L #) as SubRelStr of L by Def13; take S ; ::_thesis: ( S is strict & S is full ) thus S is strict ; ::_thesis: S is full thus the InternalRel of S = the InternalRel of L |_2 the carrier of S by XBOOLE_1:28; :: according to YELLOW_0:def_14 ::_thesis: verum end; end; registration let L be non empty RelStr ; cluster non empty strict full for SubRelStr of L; existence ex b1 being SubRelStr of L st ( not b1 is empty & b1 is full & b1 is strict ) proof set S = RelStr(# the carrier of L, the InternalRel of L #); reconsider S = RelStr(# the carrier of L, the InternalRel of L #) as SubRelStr of L by Def13; take S ; ::_thesis: ( not S is empty & S is full & S is strict ) thus not the carrier of S is empty ; :: according to STRUCT_0:def_1 ::_thesis: ( S is full & S is strict ) thus the InternalRel of S = the InternalRel of L |_2 the carrier of S by XBOOLE_1:28; :: according to YELLOW_0:def_14 ::_thesis: S is strict thus S is strict ; ::_thesis: verum end; end; theorem Th56: :: YELLOW_0:56 for L being RelStr for X being Subset of L holds RelStr(# X,( the InternalRel of L |_2 X) #) is full SubRelStr of L proof let L be RelStr ; ::_thesis: for X being Subset of L holds RelStr(# X,( the InternalRel of L |_2 X) #) is full SubRelStr of L let X be Subset of L; ::_thesis: RelStr(# X,( the InternalRel of L |_2 X) #) is full SubRelStr of L set S = RelStr(# X,( the InternalRel of L |_2 X) #); the InternalRel of RelStr(# X,( the InternalRel of L |_2 X) #) c= the InternalRel of L by XBOOLE_1:17; then reconsider S = RelStr(# X,( the InternalRel of L |_2 X) #) as SubRelStr of L by Def13; S is full by Def14; hence RelStr(# X,( the InternalRel of L |_2 X) #) is full SubRelStr of L ; ::_thesis: verum end; theorem Th57: :: YELLOW_0:57 for L being RelStr for S1, S2 being full SubRelStr of L st the carrier of S1 = the carrier of S2 holds RelStr(# the carrier of S1, the InternalRel of S1 #) = RelStr(# the carrier of S2, the InternalRel of S2 #) proof let L be RelStr ; ::_thesis: for S1, S2 being full SubRelStr of L st the carrier of S1 = the carrier of S2 holds RelStr(# the carrier of S1, the InternalRel of S1 #) = RelStr(# the carrier of S2, the InternalRel of S2 #) let S1, S2 be full SubRelStr of L; ::_thesis: ( the carrier of S1 = the carrier of S2 implies RelStr(# the carrier of S1, the InternalRel of S1 #) = RelStr(# the carrier of S2, the InternalRel of S2 #) ) the InternalRel of S1 = the InternalRel of L |_2 the carrier of S1 by Def14; hence ( the carrier of S1 = the carrier of S2 implies RelStr(# the carrier of S1, the InternalRel of S1 #) = RelStr(# the carrier of S2, the InternalRel of S2 #) ) by Def14; ::_thesis: verum end; definition let L be RelStr ; let X be Subset of L; func subrelstr X -> strict full SubRelStr of L means :: YELLOW_0:def 15 the carrier of it = X; uniqueness for b1, b2 being strict full SubRelStr of L st the carrier of b1 = X & the carrier of b2 = X holds b1 = b2 by Th57; existence ex b1 being strict full SubRelStr of L st the carrier of b1 = X proof RelStr(# X,( the InternalRel of L |_2 X) #) is full SubRelStr of L by Th56; hence ex b1 being strict full SubRelStr of L st the carrier of b1 = X ; ::_thesis: verum end; end; :: deftheorem defines subrelstr YELLOW_0:def_15_:_ for L being RelStr for X being Subset of L for b3 being strict full SubRelStr of L holds ( b3 = subrelstr X iff the carrier of b3 = X ); theorem Th58: :: YELLOW_0:58 for L being non empty RelStr for S being non empty SubRelStr of L for x being Element of S holds x is Element of L proof let L be non empty RelStr ; ::_thesis: for S being non empty SubRelStr of L for x being Element of S holds x is Element of L let S be non empty SubRelStr of L; ::_thesis: for x being Element of S holds x is Element of L let x be Element of S; ::_thesis: x is Element of L ( x in the carrier of S & the carrier of S c= the carrier of L ) by Def13; hence x is Element of L ; ::_thesis: verum end; theorem Th59: :: YELLOW_0:59 for L being RelStr for S being SubRelStr of L for a, b being Element of L for x, y being Element of S st x = a & y = b & x <= y holds a <= b proof let L be RelStr ; ::_thesis: for S being SubRelStr of L for a, b being Element of L for x, y being Element of S st x = a & y = b & x <= y holds a <= b let S be SubRelStr of L; ::_thesis: for a, b being Element of L for x, y being Element of S st x = a & y = b & x <= y holds a <= b let a, b be Element of L; ::_thesis: for x, y being Element of S st x = a & y = b & x <= y holds a <= b let x, y be Element of S; ::_thesis: ( x = a & y = b & x <= y implies a <= b ) assume A1: ( x = a & y = b ) ; ::_thesis: ( not x <= y or a <= b ) A2: the InternalRel of S c= the InternalRel of L by Def13; assume [x,y] in the InternalRel of S ; :: according to ORDERS_2:def_5 ::_thesis: a <= b hence [a,b] in the InternalRel of L by A1, A2; :: according to ORDERS_2:def_5 ::_thesis: verum end; theorem Th60: :: YELLOW_0:60 for L being RelStr for S being full SubRelStr of L for a, b being Element of L for x, y being Element of S st x = a & y = b & a <= b & x in the carrier of S holds x <= y proof let L be RelStr ; ::_thesis: for S being full SubRelStr of L for a, b being Element of L for x, y being Element of S st x = a & y = b & a <= b & x in the carrier of S holds x <= y let S be full SubRelStr of L; ::_thesis: for a, b being Element of L for x, y being Element of S st x = a & y = b & a <= b & x in the carrier of S holds x <= y let a, b be Element of L; ::_thesis: for x, y being Element of S st x = a & y = b & a <= b & x in the carrier of S holds x <= y let x, y be Element of S; ::_thesis: ( x = a & y = b & a <= b & x in the carrier of S implies x <= y ) assume A1: ( x = a & y = b ) ; ::_thesis: ( not a <= b or not x in the carrier of S or x <= y ) assume A2: [a,b] in the InternalRel of L ; :: according to ORDERS_2:def_5 ::_thesis: ( not x in the carrier of S or x <= y ) A3: the InternalRel of S = the InternalRel of L |_2 the carrier of S by Def14; assume x in the carrier of S ; ::_thesis: x <= y then [x,y] in [: the carrier of S, the carrier of S:] by ZFMISC_1:87; hence [x,y] in the InternalRel of S by A1, A3, A2, XBOOLE_0:def_4; :: according to ORDERS_2:def_5 ::_thesis: verum end; theorem Th61: :: YELLOW_0:61 for L being non empty RelStr for S being non empty full SubRelStr of L for X being set for a being Element of L for x being Element of S st x = a holds ( ( a is_<=_than X implies x is_<=_than X ) & ( a is_>=_than X implies x is_>=_than X ) ) proof let L be non empty RelStr ; ::_thesis: for S being non empty full SubRelStr of L for X being set for a being Element of L for x being Element of S st x = a holds ( ( a is_<=_than X implies x is_<=_than X ) & ( a is_>=_than X implies x is_>=_than X ) ) let S be non empty full SubRelStr of L; ::_thesis: for X being set for a being Element of L for x being Element of S st x = a holds ( ( a is_<=_than X implies x is_<=_than X ) & ( a is_>=_than X implies x is_>=_than X ) ) let X be set ; ::_thesis: for a being Element of L for x being Element of S st x = a holds ( ( a is_<=_than X implies x is_<=_than X ) & ( a is_>=_than X implies x is_>=_than X ) ) let a be Element of L; ::_thesis: for x being Element of S st x = a holds ( ( a is_<=_than X implies x is_<=_than X ) & ( a is_>=_than X implies x is_>=_than X ) ) let x be Element of S; ::_thesis: ( x = a implies ( ( a is_<=_than X implies x is_<=_than X ) & ( a is_>=_than X implies x is_>=_than X ) ) ) assume A1: x = a ; ::_thesis: ( ( a is_<=_than X implies x is_<=_than X ) & ( a is_>=_than X implies x is_>=_than X ) ) hereby ::_thesis: ( a is_>=_than X implies x is_>=_than X ) assume A2: a is_<=_than X ; ::_thesis: x is_<=_than X thus x is_<=_than X ::_thesis: verum proof let y be Element of S; :: according to LATTICE3:def_8 ::_thesis: ( not y in X or x <= y ) reconsider b = y as Element of L by Th58; assume y in X ; ::_thesis: x <= y then a <= b by A2, LATTICE3:def_8; hence x <= y by A1, Th60; ::_thesis: verum end; end; assume A3: a is_>=_than X ; ::_thesis: x is_>=_than X let y be Element of S; :: according to LATTICE3:def_9 ::_thesis: ( not y in X or y <= x ) reconsider b = y as Element of L by Th58; assume y in X ; ::_thesis: y <= x then a >= b by A3, LATTICE3:def_9; hence y <= x by A1, Th60; ::_thesis: verum end; theorem Th62: :: YELLOW_0:62 for L being non empty RelStr for S being non empty SubRelStr of L for X being Subset of S for a being Element of L for x being Element of S st x = a holds ( ( x is_<=_than X implies a is_<=_than X ) & ( x is_>=_than X implies a is_>=_than X ) ) proof let L be non empty RelStr ; ::_thesis: for S being non empty SubRelStr of L for X being Subset of S for a being Element of L for x being Element of S st x = a holds ( ( x is_<=_than X implies a is_<=_than X ) & ( x is_>=_than X implies a is_>=_than X ) ) let S be non empty SubRelStr of L; ::_thesis: for X being Subset of S for a being Element of L for x being Element of S st x = a holds ( ( x is_<=_than X implies a is_<=_than X ) & ( x is_>=_than X implies a is_>=_than X ) ) let X be Subset of S; ::_thesis: for a being Element of L for x being Element of S st x = a holds ( ( x is_<=_than X implies a is_<=_than X ) & ( x is_>=_than X implies a is_>=_than X ) ) let a be Element of L; ::_thesis: for x being Element of S st x = a holds ( ( x is_<=_than X implies a is_<=_than X ) & ( x is_>=_than X implies a is_>=_than X ) ) let x be Element of S; ::_thesis: ( x = a implies ( ( x is_<=_than X implies a is_<=_than X ) & ( x is_>=_than X implies a is_>=_than X ) ) ) assume A1: x = a ; ::_thesis: ( ( x is_<=_than X implies a is_<=_than X ) & ( x is_>=_than X implies a is_>=_than X ) ) hereby ::_thesis: ( x is_>=_than X implies a is_>=_than X ) assume A2: x is_<=_than X ; ::_thesis: a is_<=_than X thus a is_<=_than X ::_thesis: verum proof let b be Element of L; :: according to LATTICE3:def_8 ::_thesis: ( not b in X or a <= b ) assume A3: b in X ; ::_thesis: a <= b then reconsider y = b as Element of S ; x <= y by A2, A3, LATTICE3:def_8; hence a <= b by A1, Th59; ::_thesis: verum end; end; assume A4: x is_>=_than X ; ::_thesis: a is_>=_than X let b be Element of L; :: according to LATTICE3:def_9 ::_thesis: ( not b in X or b <= a ) assume A5: b in X ; ::_thesis: b <= a then reconsider y = b as Element of S ; x >= y by A4, A5, LATTICE3:def_9; hence b <= a by A1, Th59; ::_thesis: verum end; registration let L be reflexive RelStr ; cluster full -> reflexive full for SubRelStr of L; coherence for b1 being full SubRelStr of L holds b1 is reflexive proof let S be full SubRelStr of L; ::_thesis: S is reflexive let x be set ; :: according to RELAT_2:def_1,ORDERS_2:def_2 ::_thesis: ( not x in the carrier of S or [x,x] in the InternalRel of S ) assume A1: x in the carrier of S ; ::_thesis: [x,x] in the InternalRel of S then A2: [x,x] in [: the carrier of S, the carrier of S:] by ZFMISC_1:87; ( the carrier of S c= the carrier of L & the InternalRel of L is_reflexive_in the carrier of L ) by Def13, ORDERS_2:def_2; then A3: [x,x] in the InternalRel of L by A1, RELAT_2:def_1; the InternalRel of S = the InternalRel of L |_2 the carrier of S by Def14; hence [x,x] in the InternalRel of S by A2, A3, XBOOLE_0:def_4; ::_thesis: verum end; end; registration let L be transitive RelStr ; cluster full -> transitive full for SubRelStr of L; coherence for b1 being full SubRelStr of L holds b1 is transitive proof let S be full SubRelStr of L; ::_thesis: S is transitive let x, y, z be Element of S; :: according to YELLOW_0:def_2 ::_thesis: ( x <= y & y <= z implies x <= z ) assume that A1: x <= y and A2: y <= z ; ::_thesis: x <= z A3: the carrier of S c= the carrier of L by Def13; [y,z] in the InternalRel of S by A2, ORDERS_2:def_5; then A4: z in the carrier of S by ZFMISC_1:87; A5: [x,y] in the InternalRel of S by A1, ORDERS_2:def_5; then A6: x in the carrier of S by ZFMISC_1:87; y in the carrier of S by A5, ZFMISC_1:87; then reconsider a = x, b = y, c = z as Element of L by A6, A4, A3; ( a <= b & b <= c ) by A1, A2, Th59; hence x <= z by A6, Th60, ORDERS_2:3; ::_thesis: verum end; end; registration let L be antisymmetric RelStr ; cluster full -> antisymmetric full for SubRelStr of L; coherence for b1 being full SubRelStr of L holds b1 is antisymmetric proof let S be full SubRelStr of L; ::_thesis: S is antisymmetric let x, y be Element of S; :: according to YELLOW_0:def_3 ::_thesis: ( x <= y & y <= x implies x = y ) assume that A1: x <= y and A2: y <= x ; ::_thesis: x = y A3: the carrier of S c= the carrier of L by Def13; [x,y] in the InternalRel of S by A1, ORDERS_2:def_5; then ( x in the carrier of S & y in the carrier of S ) by ZFMISC_1:87; then reconsider a = x, b = y as Element of L by A3; ( a <= b & b <= a ) by A1, A2, Th59; hence x = y by ORDERS_2:2; ::_thesis: verum end; end; definition let L be non empty RelStr ; let S be SubRelStr of L; attrS is meet-inheriting means :Def16: :: YELLOW_0:def 16 for x, y being Element of L st x in the carrier of S & y in the carrier of S & ex_inf_of {x,y},L holds inf {x,y} in the carrier of S; attrS is join-inheriting means :Def17: :: YELLOW_0:def 17 for x, y being Element of L st x in the carrier of S & y in the carrier of S & ex_sup_of {x,y},L holds sup {x,y} in the carrier of S; end; :: deftheorem Def16 defines meet-inheriting YELLOW_0:def_16_:_ for L being non empty RelStr for S being SubRelStr of L holds ( S is meet-inheriting iff for x, y being Element of L st x in the carrier of S & y in the carrier of S & ex_inf_of {x,y},L holds inf {x,y} in the carrier of S ); :: deftheorem Def17 defines join-inheriting YELLOW_0:def_17_:_ for L being non empty RelStr for S being SubRelStr of L holds ( S is join-inheriting iff for x, y being Element of L st x in the carrier of S & y in the carrier of S & ex_sup_of {x,y},L holds sup {x,y} in the carrier of S ); definition let L be non empty RelStr ; let S be SubRelStr of L; attrS is infs-inheriting means :: YELLOW_0:def 18 for X being Subset of S st ex_inf_of X,L holds "/\" (X,L) in the carrier of S; attrS is sups-inheriting means :: YELLOW_0:def 19 for X being Subset of S st ex_sup_of X,L holds "\/" (X,L) in the carrier of S; end; :: deftheorem defines infs-inheriting YELLOW_0:def_18_:_ for L being non empty RelStr for S being SubRelStr of L holds ( S is infs-inheriting iff for X being Subset of S st ex_inf_of X,L holds "/\" (X,L) in the carrier of S ); :: deftheorem defines sups-inheriting YELLOW_0:def_19_:_ for L being non empty RelStr for S being SubRelStr of L holds ( S is sups-inheriting iff for X being Subset of S st ex_sup_of X,L holds "\/" (X,L) in the carrier of S ); registration let L be non empty RelStr ; cluster infs-inheriting -> meet-inheriting for SubRelStr of L; coherence for b1 being SubRelStr of L st b1 is infs-inheriting holds b1 is meet-inheriting proof let S be SubRelStr of L; ::_thesis: ( S is infs-inheriting implies S is meet-inheriting ) assume A1: for X being Subset of S st ex_inf_of X,L holds "/\" (X,L) in the carrier of S ; :: according to YELLOW_0:def_18 ::_thesis: S is meet-inheriting let x, y be Element of L; :: according to YELLOW_0:def_16 ::_thesis: ( x in the carrier of S & y in the carrier of S & ex_inf_of {x,y},L implies inf {x,y} in the carrier of S ) assume ( x in the carrier of S & y in the carrier of S ) ; ::_thesis: ( not ex_inf_of {x,y},L or inf {x,y} in the carrier of S ) then {x,y} c= the carrier of S by ZFMISC_1:32; hence ( not ex_inf_of {x,y},L or inf {x,y} in the carrier of S ) by A1; ::_thesis: verum end; cluster sups-inheriting -> join-inheriting for SubRelStr of L; coherence for b1 being SubRelStr of L st b1 is sups-inheriting holds b1 is join-inheriting proof let S be SubRelStr of L; ::_thesis: ( S is sups-inheriting implies S is join-inheriting ) assume A2: for X being Subset of S st ex_sup_of X,L holds "\/" (X,L) in the carrier of S ; :: according to YELLOW_0:def_19 ::_thesis: S is join-inheriting let x, y be Element of L; :: according to YELLOW_0:def_17 ::_thesis: ( x in the carrier of S & y in the carrier of S & ex_sup_of {x,y},L implies sup {x,y} in the carrier of S ) assume ( x in the carrier of S & y in the carrier of S ) ; ::_thesis: ( not ex_sup_of {x,y},L or sup {x,y} in the carrier of S ) then {x,y} c= the carrier of S by ZFMISC_1:32; hence ( not ex_sup_of {x,y},L or sup {x,y} in the carrier of S ) by A2; ::_thesis: verum end; end; registration let L be non empty RelStr ; cluster non empty strict full infs-inheriting sups-inheriting for 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 ( the carrier of L c= the carrier of L & the InternalRel of L |_2 the carrier of L = the InternalRel of L ) by XBOOLE_1:28; then reconsider S = RelStr(# the carrier of L, the InternalRel of L #) as non empty strict full SubRelStr of L by Th56; take S ; ::_thesis: ( S is infs-inheriting & S is sups-inheriting & not S is empty & S is full & S is strict ) thus S is infs-inheriting ::_thesis: ( S is sups-inheriting & not S is empty & S is full & S is strict ) proof let X be Subset of S; :: according to YELLOW_0:def_18 ::_thesis: ( ex_inf_of X,L implies "/\" (X,L) in the carrier of S ) thus ( ex_inf_of X,L implies "/\" (X,L) in the carrier of S ) ; ::_thesis: verum end; thus S is sups-inheriting ::_thesis: ( not S is empty & S is full & S is strict ) proof let X be Subset of S; :: according to YELLOW_0:def_19 ::_thesis: ( ex_sup_of X,L implies "\/" (X,L) in the carrier of S ) thus ( ex_sup_of X,L implies "\/" (X,L) in the carrier of S ) ; ::_thesis: verum end; thus ( not S is empty & S is full & S is strict ) ; ::_thesis: verum end; end; theorem Th63: :: YELLOW_0:63 for L being non empty transitive RelStr for S being non empty full SubRelStr of L for X being Subset of S st ex_inf_of X,L & "/\" (X,L) in the carrier of S holds ( ex_inf_of X,S & "/\" (X,S) = "/\" (X,L) ) proof let L be non empty transitive RelStr ; ::_thesis: for S being non empty full SubRelStr of L for X being Subset of S st ex_inf_of X,L & "/\" (X,L) in the carrier of S holds ( ex_inf_of X,S & "/\" (X,S) = "/\" (X,L) ) let S be non empty full SubRelStr of L; ::_thesis: for X being Subset of S st ex_inf_of X,L & "/\" (X,L) in the carrier of S holds ( ex_inf_of X,S & "/\" (X,S) = "/\" (X,L) ) let X be Subset of S; ::_thesis: ( ex_inf_of X,L & "/\" (X,L) in the carrier of S implies ( ex_inf_of X,S & "/\" (X,S) = "/\" (X,L) ) ) assume that A1: ex_inf_of X,L and A2: "/\" (X,L) in the carrier of S ; ::_thesis: ( ex_inf_of X,S & "/\" (X,S) = "/\" (X,L) ) reconsider a = "/\" (X,L) as Element of S by A2; A3: now__::_thesis:_(_a_is_<=_than_X_&_(_for_b_being_Element_of_S_st_b_is_<=_than_X_holds_ b_<=_a_)_) "/\" (X,L) is_<=_than X by A1, Def10; hence a is_<=_than X by Th61; ::_thesis: for b being Element of S st b is_<=_than X holds b <= a let b be Element of S; ::_thesis: ( b is_<=_than X implies b <= a ) reconsider b9 = b as Element of L by Th58; assume b is_<=_than X ; ::_thesis: b <= a then b9 is_<=_than X by Th62; then b9 <= "/\" (X,L) by A1, Def10; hence b <= a by Th60; ::_thesis: verum end; consider a9 being Element of L such that A4: X is_>=_than a9 and A5: for b being Element of L st X is_>=_than b holds b <= a9 and for c being Element of L st X is_>=_than c & ( for b being Element of L st X is_>=_than b holds b <= c ) holds c = a9 by A1, Def8; A6: a9 = "/\" (X,L) by A1, A4, A5, Def10; thus ex_inf_of X,S ::_thesis: "/\" (X,S) = "/\" (X,L) proof take a ; :: according to YELLOW_0:def_8 ::_thesis: ( X is_>=_than a & ( for b being Element of S st X is_>=_than b holds b <= a ) & ( for c being Element of S st X is_>=_than c & ( for b being Element of S st X is_>=_than b holds b <= c ) holds c = a ) ) thus ( a is_<=_than X & ( for b being Element of S st b is_<=_than X holds b <= a ) ) by A3; ::_thesis: for c being Element of S st X is_>=_than c & ( for b being Element of S st X is_>=_than b holds b <= c ) holds c = a let c be Element of S; ::_thesis: ( X is_>=_than c & ( for b being Element of S st X is_>=_than b holds b <= c ) implies c = a ) reconsider c9 = c as Element of L by Th58; assume X is_>=_than c ; ::_thesis: ( ex b being Element of S st ( X is_>=_than b & not b <= c ) or c = a ) then A7: X is_>=_than c9 by Th62; assume for b being Element of S st X is_>=_than b holds b <= c ; ::_thesis: c = a then A8: a <= c by A3; now__::_thesis:_for_b_being_Element_of_L_st_X_is_>=_than_b_holds_ b_<=_c9 let b be Element of L; ::_thesis: ( X is_>=_than b implies b <= c9 ) assume X is_>=_than b ; ::_thesis: b <= c9 then A9: b <= a9 by A5; a9 <= c9 by A6, A8, Th59; hence b <= c9 by A9, ORDERS_2:3; ::_thesis: verum end; hence c = a by A1, A7, Def10; ::_thesis: verum end; hence "/\" (X,S) = "/\" (X,L) by A3, Def10; ::_thesis: verum end; theorem Th64: :: YELLOW_0:64 for L being non empty transitive RelStr for S being non empty full SubRelStr of L for X being Subset of S st ex_sup_of X,L & "\/" (X,L) in the carrier of S holds ( ex_sup_of X,S & "\/" (X,S) = "\/" (X,L) ) proof let L be non empty transitive RelStr ; ::_thesis: for S being non empty full SubRelStr of L for X being Subset of S st ex_sup_of X,L & "\/" (X,L) in the carrier of S holds ( ex_sup_of X,S & "\/" (X,S) = "\/" (X,L) ) let S be non empty full SubRelStr of L; ::_thesis: for X being Subset of S st ex_sup_of X,L & "\/" (X,L) in the carrier of S holds ( ex_sup_of X,S & "\/" (X,S) = "\/" (X,L) ) let X be Subset of S; ::_thesis: ( ex_sup_of X,L & "\/" (X,L) in the carrier of S implies ( ex_sup_of X,S & "\/" (X,S) = "\/" (X,L) ) ) assume that A1: ex_sup_of X,L and A2: "\/" (X,L) in the carrier of S ; ::_thesis: ( ex_sup_of X,S & "\/" (X,S) = "\/" (X,L) ) reconsider a = "\/" (X,L) as Element of S by A2; A3: now__::_thesis:_(_a_is_>=_than_X_&_(_for_b_being_Element_of_S_st_b_is_>=_than_X_holds_ b_>=_a_)_) "\/" (X,L) is_>=_than X by A1, Def9; hence a is_>=_than X by Th61; ::_thesis: for b being Element of S st b is_>=_than X holds b >= a let b be Element of S; ::_thesis: ( b is_>=_than X implies b >= a ) reconsider b9 = b as Element of L by Th58; assume b is_>=_than X ; ::_thesis: b >= a then b9 is_>=_than X by Th62; then b9 >= "\/" (X,L) by A1, Def9; hence b >= a by Th60; ::_thesis: verum end; consider a9 being Element of L such that A4: X is_<=_than a9 and A5: for b being Element of L st X is_<=_than b holds b >= a9 and for c being Element of L st X is_<=_than c & ( for b being Element of L st X is_<=_than b holds b >= c ) holds c = a9 by A1, Def7; A6: a9 = "\/" (X,L) by A1, A4, A5, Def9; thus ex_sup_of X,S ::_thesis: "\/" (X,S) = "\/" (X,L) proof take a ; :: according to YELLOW_0:def_7 ::_thesis: ( X is_<=_than a & ( for b being Element of S st X is_<=_than b holds b >= a ) & ( for c being Element of S st X is_<=_than c & ( for b being Element of S st X is_<=_than b holds b >= c ) holds c = a ) ) thus ( a is_>=_than X & ( for b being Element of S st b is_>=_than X holds b >= a ) ) by A3; ::_thesis: for c being Element of S st X is_<=_than c & ( for b being Element of S st X is_<=_than b holds b >= c ) holds c = a let c be Element of S; ::_thesis: ( X is_<=_than c & ( for b being Element of S st X is_<=_than b holds b >= c ) implies c = a ) reconsider c9 = c as Element of L by Th58; assume X is_<=_than c ; ::_thesis: ( ex b being Element of S st ( X is_<=_than b & not b >= c ) or c = a ) then A7: X is_<=_than c9 by Th62; assume for b being Element of S st X is_<=_than b holds b >= c ; ::_thesis: c = a then A8: a >= c by A3; now__::_thesis:_for_b_being_Element_of_L_st_X_is_<=_than_b_holds_ b_>=_c9 let b be Element of L; ::_thesis: ( X is_<=_than b implies b >= c9 ) assume X is_<=_than b ; ::_thesis: b >= c9 then A9: b >= a9 by A5; a9 >= c9 by A6, A8, Th59; hence b >= c9 by A9, ORDERS_2:3; ::_thesis: verum end; hence c = a by A1, A7, Def9; ::_thesis: verum end; hence "\/" (X,S) = "\/" (X,L) by A3, Def9; ::_thesis: verum end; theorem :: YELLOW_0:65 for L being non empty transitive RelStr for S being non empty full SubRelStr of L for x, y being Element of S st ex_inf_of {x,y},L & "/\" ({x,y},L) in the carrier of S holds ( ex_inf_of {x,y},S & "/\" ({x,y},S) = "/\" ({x,y},L) ) by Th63; theorem :: YELLOW_0:66 for L being non empty transitive RelStr for S being non empty full SubRelStr of L for x, y being Element of S st ex_sup_of {x,y},L & "\/" ({x,y},L) in the carrier of S holds ( ex_sup_of {x,y},S & "\/" ({x,y},S) = "\/" ({x,y},L) ) by Th64; registration let L be transitive antisymmetric with_infima RelStr ; cluster non empty full meet-inheriting -> non empty with_infima full meet-inheriting for SubRelStr of L; coherence for b1 being non empty full meet-inheriting SubRelStr of L holds b1 is with_infima proof let S be non empty full meet-inheriting SubRelStr of L; ::_thesis: S is with_infima now__::_thesis:_for_x,_y_being_Element_of_S_holds_ex_inf_of_{x,y},S let x, y be Element of S; ::_thesis: ex_inf_of {x,y},S reconsider a = x, b = y as Element of L by Th58; A1: ex_inf_of {a,b},L by Th21; then "/\" ({a,b},L) in the carrier of S by Def16; hence ex_inf_of {x,y},S by A1, Th63; ::_thesis: verum end; hence S is with_infima by Th21; ::_thesis: verum end; end; registration let L be transitive antisymmetric with_suprema RelStr ; cluster non empty full join-inheriting -> non empty with_suprema full join-inheriting for SubRelStr of L; coherence for b1 being non empty full join-inheriting SubRelStr of L holds b1 is with_suprema proof let S be non empty full join-inheriting SubRelStr of L; ::_thesis: S is with_suprema now__::_thesis:_for_x,_y_being_Element_of_S_holds_ex_sup_of_{x,y},S let x, y be Element of S; ::_thesis: ex_sup_of {x,y},S reconsider a = x, b = y as Element of L by Th58; A1: ex_sup_of {a,b},L by Th20; then "\/" ({a,b},L) in the carrier of S by Def17; hence ex_sup_of {x,y},S by A1, Th64; ::_thesis: verum end; hence S is with_suprema by Th20; ::_thesis: verum end; end; theorem :: YELLOW_0:67 for L being non empty complete Poset for S being non empty full SubRelStr of L for X being Subset of S st "/\" (X,L) in the carrier of S holds "/\" (X,S) = "/\" (X,L) proof let L be non empty complete Poset; ::_thesis: for S being non empty full SubRelStr of L for X being Subset of S st "/\" (X,L) in the carrier of S holds "/\" (X,S) = "/\" (X,L) let S be non empty full SubRelStr of L; ::_thesis: for X being Subset of S st "/\" (X,L) in the carrier of S holds "/\" (X,S) = "/\" (X,L) let X be Subset of S; ::_thesis: ( "/\" (X,L) in the carrier of S implies "/\" (X,S) = "/\" (X,L) ) assume A1: "/\" (X,L) in the carrier of S ; ::_thesis: "/\" (X,S) = "/\" (X,L) ex_inf_of X,L by Th17; hence "/\" (X,S) = "/\" (X,L) by A1, Th63; ::_thesis: verum end; theorem :: YELLOW_0:68 for L being non empty complete Poset for S being non empty full SubRelStr of L for X being Subset of S st "\/" (X,L) in the carrier of S holds "\/" (X,S) = "\/" (X,L) proof let L be non empty complete Poset; ::_thesis: for S being non empty full SubRelStr of L for X being Subset of S st "\/" (X,L) in the carrier of S holds "\/" (X,S) = "\/" (X,L) let S be non empty full SubRelStr of L; ::_thesis: for X being Subset of S st "\/" (X,L) in the carrier of S holds "\/" (X,S) = "\/" (X,L) let X be Subset of S; ::_thesis: ( "\/" (X,L) in the carrier of S implies "\/" (X,S) = "\/" (X,L) ) assume A1: "\/" (X,L) in the carrier of S ; ::_thesis: "\/" (X,S) = "\/" (X,L) ex_sup_of X,L by Th17; hence "\/" (X,S) = "\/" (X,L) by A1, Th64; ::_thesis: verum end; theorem :: YELLOW_0:69 for L being with_infima Poset for S being non empty full meet-inheriting SubRelStr of L for x, y being Element of S for a, b being Element of L st a = x & b = y holds x "/\" y = a "/\" b proof let L be with_infima Poset; ::_thesis: for S being non empty full meet-inheriting SubRelStr of L for x, y being Element of S for a, b being Element of L st a = x & b = y holds x "/\" y = a "/\" b let S be non empty full meet-inheriting SubRelStr of L; ::_thesis: for x, y being Element of S for a, b being Element of L st a = x & b = y holds x "/\" y = a "/\" b let x, y be Element of S; ::_thesis: for a, b being Element of L st a = x & b = y holds x "/\" y = a "/\" b let a, b be Element of L; ::_thesis: ( a = x & b = y implies x "/\" y = a "/\" b ) assume A1: ( a = x & b = y ) ; ::_thesis: x "/\" y = a "/\" b A2: ex_inf_of {a,b},L by Th21; then "/\" ({x,y},L) in the carrier of S by A1, Def16; then A3: "/\" ({x,y},S) = "/\" ({x,y},L) by A1, A2, Th63; a "/\" b = inf {a,b} by Th40; hence x "/\" y = a "/\" b by A1, A3, Th40; ::_thesis: verum end; theorem :: YELLOW_0:70 for L being with_suprema Poset for S being non empty full join-inheriting SubRelStr of L for x, y being Element of S for a, b being Element of L st a = x & b = y holds x "\/" y = a "\/" b proof let L be with_suprema Poset; ::_thesis: for S being non empty full join-inheriting SubRelStr of L for x, y being Element of S for a, b being Element of L st a = x & b = y holds x "\/" y = a "\/" b let S be non empty full join-inheriting SubRelStr of L; ::_thesis: for x, y being Element of S for a, b being Element of L st a = x & b = y holds x "\/" y = a "\/" b let x, y be Element of S; ::_thesis: for a, b being Element of L st a = x & b = y holds x "\/" y = a "\/" b let a, b be Element of L; ::_thesis: ( a = x & b = y implies x "\/" y = a "\/" b ) assume A1: ( a = x & b = y ) ; ::_thesis: x "\/" y = a "\/" b A2: ex_sup_of {a,b},L by Th20; then "\/" ({x,y},L) in the carrier of S by A1, Def17; then A3: "\/" ({x,y},S) = "\/" ({x,y},L) by A1, A2, Th64; a "\/" b = sup {a,b} by Th41; hence x "\/" y = a "\/" b by A1, A3, Th41; ::_thesis: verum end;