:: 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;