:: YELLOW_4 semantic presentation

begin

theorem Th1: :: YELLOW_4:1
for L being RelStr
for X being set
for a being Element of L st a in X & ex_sup_of X,L holds
a <= "\/" (X,L)
proof
let L be RelStr ; ::_thesis: for X being set
for a being Element of L st a in X & ex_sup_of X,L holds
a <= "\/" (X,L)
let X be set ; ::_thesis: for a being Element of L st a in X & ex_sup_of X,L holds
a <= "\/" (X,L)
let a be Element of L; ::_thesis: ( a in X & ex_sup_of X,L implies a <= "\/" (X,L) )
assume that
A1: a in X and
A2: ex_sup_of X,L ; ::_thesis: a <= "\/" (X,L)
 X is_<=_than "\/" (X,L) by A2, YELLOW_0:def_9;
hence  a <= "\/" (X,L) by A1, LATTICE3:def_9; ::_thesis: verum
end;

theorem Th2: :: YELLOW_4:2
for L being RelStr
for X being set
for a being Element of L st a in X & ex_inf_of X,L holds
"/\" (X,L) <= a
proof
let L be RelStr ; ::_thesis: for X being set
for a being Element of L st a in X & ex_inf_of X,L holds
"/\" (X,L) <= a
let X be set ; ::_thesis: for a being Element of L st a in X & ex_inf_of X,L holds
"/\" (X,L) <= a
let a be Element of L; ::_thesis: ( a in X & ex_inf_of X,L implies "/\" (X,L) <= a )
assume that
A1: a in X and
A2: ex_inf_of X,L ; ::_thesis: "/\" (X,L) <= a
 X is_>=_than "/\" (X,L) by A2, YELLOW_0:def_10;
hence  "/\" (X,L) <= a by A1, LATTICE3:def_8; ::_thesis: verum
end;

definition
let L be RelStr ;
let A, B be Subset of L;
predA is_finer_than B means :Def1: :: YELLOW_4:def 1
 for a being Element of L st a in A holds
ex b being Element of L st
( b in B & a <= b );
predB is_coarser_than A means :Def2: :: YELLOW_4:def 2
 for b being Element of L st b in B holds
ex a being Element of L st
( a in A & a <= b );
end;

:: deftheorem Def1 defines is_finer_than YELLOW_4:def_1_:_
 for L being RelStr
for A, B being Subset of L holds
( A is_finer_than B iff for a being Element of L st a in A holds
ex b being Element of L st
( b in B & a <= b ) );

:: deftheorem Def2 defines is_coarser_than YELLOW_4:def_2_:_
 for L being RelStr
for A, B being Subset of L holds
( B is_coarser_than A iff for b being Element of L st b in B holds
ex a being Element of L st
( a in A & a <= b ) );

definition
let L be non empty reflexive RelStr ;
let A, B be Subset of L;
:: original: is_finer_than
redefine predA is_finer_than B;
reflexivity
 for A being Subset of L holds (L,b1,b1)
proof
let A be Subset of L; ::_thesis: (L,A,A)
let a be Element of L; :: according to YELLOW_4:def_1 ::_thesis: ( a in A implies ex b being Element of L st
( b in A & a <= b ) )
assume A1: a in A ; ::_thesis: ex b being Element of L st
( b in A & a <= b )
take b = a; ::_thesis: ( b in A & a <= b )
thus  ( b in A & a <= b ) by A1; ::_thesis: verum
end;
:: original: is_coarser_than
redefine predB is_coarser_than A;
reflexivity
 for B being Subset of L holds (L,b1,b1)
proof
let A be Subset of L; ::_thesis: (L,A,A)
let a be Element of L; :: according to YELLOW_4:def_2 ::_thesis: ( a in A implies ex a being Element of L st
( a in A & a <= a ) )
assume A2: a in A ; ::_thesis: ex a being Element of L st
( a in A & a <= a )
take b = a; ::_thesis: ( b in A & b <= a )
thus  ( b in A & b <= a ) by A2; ::_thesis: verum
end;
end;

theorem :: YELLOW_4:3
for L being RelStr
for B being Subset of L holds {} L is_finer_than B
proof
let L be RelStr ; ::_thesis: for B being Subset of L holds {} L is_finer_than B
let B be Subset of L; ::_thesis: {} L is_finer_than B
let a be Element of L; :: according to YELLOW_4:def_1 ::_thesis: ( a in {} L implies ex b being Element of L st
( b in B & a <= b ) )
assume  a in {} L ; ::_thesis: ex b being Element of L st
( b in B & a <= b )
hence  ex b being Element of L st
( b in B & a <= b ) ; ::_thesis: verum
end;

theorem :: YELLOW_4:4
for L being transitive RelStr
for A, B, C being Subset of L st A is_finer_than B & B is_finer_than C holds
A is_finer_than C
proof
let L be transitive RelStr ; ::_thesis: for A, B, C being Subset of L st A is_finer_than B & B is_finer_than C holds
A is_finer_than C
let A, B, C be Subset of L; ::_thesis: ( A is_finer_than B & B is_finer_than C implies A is_finer_than C )
assume that
A1: A is_finer_than B and
A2: B is_finer_than C ; ::_thesis: A is_finer_than C
let a be Element of L; :: according to YELLOW_4:def_1 ::_thesis: ( a in A implies ex b being Element of L st
( b in C & a <= b ) )
assume  a in A ; ::_thesis: ex b being Element of L st
( b in C & a <= b )
then consider b being Element of L such that
A3: b in B and
A4: a <= b by A1, Def1;
consider c being Element of L such that
A5: ( c in C & b <= c ) by A2, A3, Def1;
take  c ; ::_thesis: ( c in C & a <= c )
thus  ( c in C & a <= c ) by A4, A5, ORDERS_2:3; ::_thesis: verum
end;

theorem :: YELLOW_4:5
for L being RelStr
for A, B being Subset of L st B is_finer_than A & A is lower holds
B c= A
proof
let L be RelStr ; ::_thesis: for A, B being Subset of L st B is_finer_than A & A is lower holds
B c= A
let A, B be Subset of L; ::_thesis: ( B is_finer_than A & A is lower implies B c= A )
assume that
A1: B is_finer_than A and
A2: A is lower ; ::_thesis: B c= A
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in B or a in A )
assume A3: a in B ; ::_thesis: a in A
then reconsider a1 = a as Element of L ;
 ex b being Element of L st
( b in A & a1 <= b ) by A1, A3, Def1;
hence  a in A by A2, WAYBEL_0:def_19; ::_thesis: verum
end;

theorem :: YELLOW_4:6
for L being RelStr
for A being Subset of L holds {} L is_coarser_than A
proof
let L be RelStr ; ::_thesis: for A being Subset of L holds {} L is_coarser_than A
let A be Subset of L; ::_thesis: {} L is_coarser_than A
let b be Element of L; :: according to YELLOW_4:def_2 ::_thesis: ( b in {} L implies ex a being Element of L st
( a in A & a <= b ) )
assume  b in {} L ; ::_thesis: ex a being Element of L st
( a in A & a <= b )
hence  ex a being Element of L st
( a in A & a <= b ) ; ::_thesis: verum
end;

theorem :: YELLOW_4:7
for L being transitive RelStr
for A, B, C being Subset of L st C is_coarser_than B & B is_coarser_than A holds
C is_coarser_than A
proof
let L be transitive RelStr ; ::_thesis: for A, B, C being Subset of L st C is_coarser_than B & B is_coarser_than A holds
C is_coarser_than A
let A, B, C be Subset of L; ::_thesis: ( C is_coarser_than B & B is_coarser_than A implies C is_coarser_than A )
assume that
A1: C is_coarser_than B and
A2: B is_coarser_than A ; ::_thesis: C is_coarser_than A
let c be Element of L; :: according to YELLOW_4:def_2 ::_thesis: ( c in C implies ex a being Element of L st
( a in A & a <= c ) )
assume  c in C ; ::_thesis: ex a being Element of L st
( a in A & a <= c )
then consider b being Element of L such that
A3: b in B and
A4: b <= c by A1, Def2;
consider a being Element of L such that
A5: ( a in A & a <= b ) by A2, A3, Def2;
take  a ; ::_thesis: ( a in A & a <= c )
thus  ( a in A & a <= c ) by A4, A5, ORDERS_2:3; ::_thesis: verum
end;

theorem :: YELLOW_4:8
for L being RelStr
for A, B being Subset of L st A is_coarser_than B & B is upper holds
A c= B
proof
let L be RelStr ; ::_thesis: for A, B being Subset of L st A is_coarser_than B & B is upper holds
A c= B
let A, B be Subset of L; ::_thesis: ( A is_coarser_than B & B is upper implies A c= B )
assume that
A1: A is_coarser_than B and
A2: B is upper ; ::_thesis: A c= B
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in A or a in B )
assume A3: a in A ; ::_thesis: a in B
then reconsider a1 = a as Element of L ;
 ex b being Element of L st
( b in B & b <= a1 ) by A1, A3, Def2;
hence  a in B by A2, WAYBEL_0:def_20; ::_thesis: verum
end;

begin

definition
let L be non empty RelStr ;
let D1, D2 be Subset of L;
funcD1 "\/" D2 ->  Subset of L equals :: YELLOW_4:def 3
 {  (x "\/" y) where x, y is Element of L : ( x in D1 & y in D2 )  }  ;
coherence
  {  (x "\/" y) where x, y is Element of L : ( x in D1 & y in D2 )  }  is Subset of L
proof
  {  (x "\/" y) where x, y is Element of L : ( x in D1 & y in D2 )  }  c= the carrier of L
proof
let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in  {  (x "\/" y) where x, y is Element of L : ( x in D1 & y in D2 )  }  or q in the carrier of L )
assume  q in  {  (x "\/" y) where x, y is Element of L : ( x in D1 & y in D2 )  }  ; ::_thesis: q in the carrier of L
then  ex a, b being Element of L st
( q = a "\/" b & a in D1 & b in D2 ) ;
hence  q in the carrier of L ; ::_thesis: verum
end;
hence   {  (x "\/" y) where x, y is Element of L : ( x in D1 & y in D2 )  }  is Subset of L ; ::_thesis: verum
end;
end;

:: deftheorem  defines "\/" YELLOW_4:def_3_:_
 for L being non empty RelStr
for D1, D2 being Subset of L holds D1 "\/" D2 =  {  (x "\/" y) where x, y is Element of L : ( x in D1 & y in D2 )  }  ;

definition
let L be antisymmetric with_suprema RelStr ;
let D1, D2 be Subset of L;
:: original: "\/"
redefine funcD1 "\/" D2 ->  Subset of L;
commutativity
 for D1, D2 being Subset of L holds D1 "\/" D2 = D2 "\/" D1
proof
let D1, D2 be Subset of L; ::_thesis: D1 "\/" D2 = D2 "\/" D1
thus  D1 "\/" D2 c= D2 "\/" D1 :: according to XBOOLE_0:def_10 ::_thesis: D2 "\/" D1 c= D1 "\/" D2
proof
let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in D1 "\/" D2 or q in D2 "\/" D1 )
assume  q in D1 "\/" D2 ; ::_thesis: q in D2 "\/" D1
then  ex x, y being Element of L st
( q = x "\/" y & x in D1 & y in D2 ) ;
hence  q in D2 "\/" D1 ; ::_thesis: verum
end;
let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in D2 "\/" D1 or q in D1 "\/" D2 )
assume  q in D2 "\/" D1 ; ::_thesis: q in D1 "\/" D2
then  ex x, y being Element of L st
( q = x "\/" y & x in D2 & y in D1 ) ;
hence  q in D1 "\/" D2 ; ::_thesis: verum
end;
end;

theorem :: YELLOW_4:9
for L being non empty RelStr
for X being Subset of L holds X "\/" ({} L) = {}
proof
let L be non empty RelStr ; ::_thesis: for X being Subset of L holds X "\/" ({} L) = {}
let X be Subset of L; ::_thesis: X "\/" ({} L) = {}
thus  X "\/" ({} L) c= {} :: according to XBOOLE_0:def_10 ::_thesis: {} c= X "\/" ({} L)
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in X "\/" ({} L) or a in {} )
assume  a in X "\/" ({} L) ; ::_thesis: a in {}
then  ex s, t being Element of L st
( a = s "\/" t & s in X & t in {} L ) ;
hence  a in {} ; ::_thesis: verum
end;
thus  {} c= X "\/" ({} L) by XBOOLE_1:2; ::_thesis: verum
end;

theorem :: YELLOW_4:10
for L being non empty RelStr
for X, Y being Subset of L
for x, y being Element of L st x in X & y in Y holds
x "\/" y in X "\/" Y ;

theorem :: YELLOW_4:11
for L being antisymmetric with_suprema RelStr
for A being Subset of L
for B being non empty Subset of L holds A is_finer_than A "\/" B
proof
let L be antisymmetric with_suprema RelStr ; ::_thesis: for A being Subset of L
for B being non empty Subset of L holds A is_finer_than A "\/" B
let A be Subset of L; ::_thesis: for B being non empty Subset of L holds A is_finer_than A "\/" B
let B be non empty Subset of L; ::_thesis: A is_finer_than A "\/" B
let q be Element of L; :: according to YELLOW_4:def_1 ::_thesis: ( q in A implies ex b being Element of L st
( b in A "\/" B & q <= b ) )
assume A1: q in A ; ::_thesis: ex b being Element of L st
( b in A "\/" B & q <= b )
set b = the Element of B;
take  q "\/" the Element of B ; ::_thesis: ( q "\/" the Element of B in A "\/" B & q <= q "\/" the Element of B )
thus  q "\/" the Element of B in A "\/" B by A1; ::_thesis: q <= q "\/" the Element of B
thus  q <= q "\/" the Element of B by YELLOW_0:22; ::_thesis: verum
end;

theorem :: YELLOW_4:12
for L being antisymmetric with_suprema RelStr
for A, B being Subset of L holds A "\/" B is_coarser_than A
proof
let L be antisymmetric with_suprema RelStr ; ::_thesis: for A, B being Subset of L holds A "\/" B is_coarser_than A
let A, B be Subset of L; ::_thesis: A "\/" B is_coarser_than A
let q be Element of L; :: according to YELLOW_4:def_2 ::_thesis: ( q in A "\/" B implies ex a being Element of L st
( a in A & a <= q ) )
assume  q in A "\/" B ; ::_thesis: ex a being Element of L st
( a in A & a <= q )
then consider x, y being Element of L such that
A1: q = x "\/" y and
A2: x in A and
 y in B ;
take  x ; ::_thesis: ( x in A & x <= q )
thus  x in A by A2; ::_thesis: x <= q
thus  x <= q by A1, YELLOW_0:22; ::_thesis: verum
end;

theorem :: YELLOW_4:13
for L being reflexive antisymmetric with_suprema RelStr
for A being Subset of L holds A c= A "\/" A
proof
let L be reflexive antisymmetric with_suprema RelStr ; ::_thesis: for A being Subset of L holds A c= A "\/" A
let A be Subset of L; ::_thesis: A c= A "\/" A
let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in A or q in A "\/" A )
assume A1: q in A ; ::_thesis: q in A "\/" A
then reconsider A1 = A as non empty Subset of L ;
reconsider q1 = q as Element of A1 by A1;
 q1 <= q1 ;
then  q1 = q1 "\/" q1 by YELLOW_0:24;
hence  q in A "\/" A ; ::_thesis: verum
end;

theorem :: YELLOW_4:14
for L being transitive antisymmetric with_suprema RelStr
for D1, D2, D3 being Subset of L holds (D1 "\/" D2) "\/" D3 = D1 "\/" (D2 "\/" D3)
proof
let L be transitive antisymmetric with_suprema RelStr ; ::_thesis: for D1, D2, D3 being Subset of L holds (D1 "\/" D2) "\/" D3 = D1 "\/" (D2 "\/" D3)
let D1, D2, D3 be Subset of L; ::_thesis: (D1 "\/" D2) "\/" D3 = D1 "\/" (D2 "\/" D3)
thus  (D1 "\/" D2) "\/" D3 c= D1 "\/" (D2 "\/" D3) :: according to XBOOLE_0:def_10 ::_thesis: D1 "\/" (D2 "\/" D3) c= (D1 "\/" D2) "\/" D3
proof
let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in (D1 "\/" D2) "\/" D3 or q in D1 "\/" (D2 "\/" D3) )
assume  q in (D1 "\/" D2) "\/" D3 ; ::_thesis: q in D1 "\/" (D2 "\/" D3)
then consider a1, b1 being Element of L such that
A1: q = a1 "\/" b1 and
A2: a1 in D1 "\/" D2 and
A3: b1 in D3 ;
consider a11, b11 being Element of L such that
A4: a1 = a11 "\/" b11 and
A5: a11 in D1 and
A6: b11 in D2 by A2;
 ( b11 "\/" b1 in D2 "\/" D3 & q = a11 "\/" (b11 "\/" b1) ) by A1, A3, A4, A6, LATTICE3:14;
hence  q in D1 "\/" (D2 "\/" D3) by A5; ::_thesis: verum
end;
let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in D1 "\/" (D2 "\/" D3) or q in (D1 "\/" D2) "\/" D3 )
assume  q in D1 "\/" (D2 "\/" D3) ; ::_thesis: q in (D1 "\/" D2) "\/" D3
then consider a1, b1 being Element of L such that
A7: ( q = a1 "\/" b1 & a1 in D1 ) and
A8: b1 in D2 "\/" D3 ;
consider a11, b11 being Element of L such that
A9: ( b1 = a11 "\/" b11 & a11 in D2 ) and
A10: b11 in D3 by A8;
 ( a1 "\/" a11 in D1 "\/" D2 & q = (a1 "\/" a11) "\/" b11 ) by A7, A9, LATTICE3:14;
hence  q in (D1 "\/" D2) "\/" D3 by A10; ::_thesis: verum
end;

registration
let L be non empty RelStr ;
let D1, D2 be non empty Subset of L;
clusterD1 "\/" D2 ->  non empty ;
coherence
 not D1 "\/" D2 is empty
proof
consider b being set  such that
A1: b in D2 by XBOOLE_0:def_1;
reconsider b = b as Element of D2 by A1;
consider a being set  such that
A2: a in D1 by XBOOLE_0:def_1;
reconsider a = a as Element of D1 by A2;
 a "\/" b in  {  (x "\/" y) where x, y is Element of L : ( x in D1 & y in D2 )  }  ;
hence  not D1 "\/" D2 is empty ; ::_thesis: verum
end;
end;

registration
let L be transitive antisymmetric with_suprema RelStr ;
let D1, D2 be directed Subset of L;
clusterD1 "\/" D2 ->  directed ;
coherence
 D1 "\/" D2 is directed
proof
let a, b be Element of L; :: according to WAYBEL_0:def_1 ::_thesis: ( not a in D1 "\/" D2 or not b in D1 "\/" D2 or ex b1 being Element of the carrier of L st
( b1 in D1 "\/" D2 & a <= b1 & b <= b1 ) )
set X = D1 "\/" D2;
assume that
A1: a in D1 "\/" D2 and
A2: b in D1 "\/" D2 ; ::_thesis: ex b1 being Element of the carrier of L st
( b1 in D1 "\/" D2 & a <= b1 & b <= b1 )
consider x, y being Element of L such that
A3: a = x "\/" y and
A4: x in D1 and
A5: y in D2 by A1;
consider s, t being Element of L such that
A6: b = s "\/" t and
A7: s in D1 and
A8: t in D2 by A2;
consider z2 being Element of L such that
A9: z2 in D2 and
A10: ( y <= z2 & t <= z2 ) by A5, A8, WAYBEL_0:def_1;
consider z1 being Element of L such that
A11: z1 in D1 and
A12: ( x <= z1 & s <= z1 ) by A4, A7, WAYBEL_0:def_1;
take z = z1 "\/" z2; ::_thesis: ( z in D1 "\/" D2 & a <= z & b <= z )
thus  z in D1 "\/" D2 by A11, A9; ::_thesis: ( a <= z & b <= z )
thus  ( a <= z & b <= z ) by A3, A6, A12, A10, YELLOW_3:3; ::_thesis: verum
end;
end;

registration
let L be transitive antisymmetric with_suprema RelStr ;
let D1, D2 be filtered Subset of L;
clusterD1 "\/" D2 ->  filtered ;
coherence
 D1 "\/" D2 is filtered
proof
let a, b be Element of L; :: according to WAYBEL_0:def_2 ::_thesis: ( not a in D1 "\/" D2 or not b in D1 "\/" D2 or ex b1 being Element of the carrier of L st
( b1 in D1 "\/" D2 & b1 <= a & b1 <= b ) )
set X = D1 "\/" D2;
assume that
A1: a in D1 "\/" D2 and
A2: b in D1 "\/" D2 ; ::_thesis: ex b1 being Element of the carrier of L st
( b1 in D1 "\/" D2 & b1 <= a & b1 <= b )
consider x, y being Element of L such that
A3: a = x "\/" y and
A4: x in D1 and
A5: y in D2 by A1;
consider s, t being Element of L such that
A6: b = s "\/" t and
A7: s in D1 and
A8: t in D2 by A2;
consider z2 being Element of L such that
A9: z2 in D2 and
A10: ( y >= z2 & t >= z2 ) by A5, A8, WAYBEL_0:def_2;
consider z1 being Element of L such that
A11: z1 in D1 and
A12: ( x >= z1 & s >= z1 ) by A4, A7, WAYBEL_0:def_2;
take z = z1 "\/" z2; ::_thesis: ( z in D1 "\/" D2 & z <= a & z <= b )
thus  z in D1 "\/" D2 by A11, A9; ::_thesis: ( z <= a & z <= b )
thus  ( z <= a & z <= b ) by A3, A6, A12, A10, YELLOW_3:3; ::_thesis: verum
end;
end;

registration
let L be with_suprema Poset;
let D1, D2 be upper Subset of L;
clusterD1 "\/" D2 ->  upper ;
coherence
 D1 "\/" D2 is upper
proof
set X = D1 "\/" D2;
let a, b be Element of L; :: according to WAYBEL_0:def_20 ::_thesis: ( not a in D1 "\/" D2 or not a <= b or b in D1 "\/" D2 )
assume that
A1: a in D1 "\/" D2 and
A2: a <= b ; ::_thesis: b in D1 "\/" D2
consider x, y being Element of L such that
A3: a = x "\/" y and
A4: x in D1 and
A5: y in D2 by A1;
A6: ex xx being Element of L st
( x <= xx & y <= xx & ( for c being Element of L st x <= c & y <= c holds
xx <= c ) ) by LATTICE3:def_10;
then  x <= x "\/" y by LATTICE3:def_13;
then  x <= b by A2, A3, YELLOW_0:def_2;
then A7: b in D1 by A4, WAYBEL_0:def_20;
 y <= x "\/" y by A6, LATTICE3:def_13;
then  y <= b by A2, A3, YELLOW_0:def_2;
then A8: b in D2 by A5, WAYBEL_0:def_20;
 b <= b ;
then  b = b "\/" b by YELLOW_0:24;
hence  b in D1 "\/" D2 by A7, A8; ::_thesis: verum
end;
end;

theorem Th15: :: YELLOW_4:15
for L being non empty RelStr
for Y being Subset of L
for x being Element of L holds {x} "\/" Y =  {  (x "\/" y) where y is Element of L : y in Y  }
proof
let L be non empty RelStr ; ::_thesis: for Y being Subset of L
for x being Element of L holds {x} "\/" Y =  {  (x "\/" y) where y is Element of L : y in Y  }
let Y be Subset of L; ::_thesis: for x being Element of L holds {x} "\/" Y =  {  (x "\/" y) where y is Element of L : y in Y  }
let x be Element of L; ::_thesis: {x} "\/" Y =  {  (x "\/" y) where y is Element of L : y in Y  }
thus  {x} "\/" Y c=  {  (x "\/" y) where y is Element of L : y in Y  }  :: according to XBOOLE_0:def_10 ::_thesis:  {  (x "\/" y) where y is Element of L : y in Y  }  c= {x} "\/" Y
proof
let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in {x} "\/" Y or q in  {  (x "\/" y) where y is Element of L : y in Y  }  )
assume  q in {x} "\/" Y ; ::_thesis: q in  {  (x "\/" y) where y is Element of L : y in Y  }
then consider s, t being Element of L such that
A1: q = s "\/" t and
A2: s in {x} and
A3: t in Y ;
 s = x by A2, TARSKI:def_1;
hence  q in  {  (x "\/" y) where y is Element of L : y in Y  }  by A1, A3; ::_thesis: verum
end;
let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in  {  (x "\/" y) where y is Element of L : y in Y  }  or q in {x} "\/" Y )
assume  q in  {  (x "\/" y) where y is Element of L : y in Y  }  ; ::_thesis: q in {x} "\/" Y
then A4: ex y being Element of L st
( q = x "\/" y & y in Y ) ;
 x in {x} by TARSKI:def_1;
hence  q in {x} "\/" Y by A4; ::_thesis: verum
end;

theorem :: YELLOW_4:16
for L being non empty RelStr
for A, B, C being Subset of L holds A "\/" (B \/ C) = (A "\/" B) \/ (A "\/" C)
proof
let L be non empty RelStr ; ::_thesis: for A, B, C being Subset of L holds A "\/" (B \/ C) = (A "\/" B) \/ (A "\/" C)
let A, B, C be Subset of L; ::_thesis: A "\/" (B \/ C) = (A "\/" B) \/ (A "\/" C)
thus  A "\/" (B \/ C) c= (A "\/" B) \/ (A "\/" C) :: according to XBOOLE_0:def_10 ::_thesis: (A "\/" B) \/ (A "\/" C) c= A "\/" (B \/ C)
proof
let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in A "\/" (B \/ C) or q in (A "\/" B) \/ (A "\/" C) )
assume  q in A "\/" (B \/ C) ; ::_thesis: q in (A "\/" B) \/ (A "\/" C)
then consider a, y being Element of L such that
A1: ( q = a "\/" y & a in A ) and
A2: y in B \/ C ;
 ( y in B or y in C ) by A2, XBOOLE_0:def_3;
then  ( q in A "\/" B or q in A "\/" C ) by A1;
hence  q in (A "\/" B) \/ (A "\/" C) by XBOOLE_0:def_3; ::_thesis: verum
end;
let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in (A "\/" B) \/ (A "\/" C) or q in A "\/" (B \/ C) )
assume A3: q in (A "\/" B) \/ (A "\/" C) ; ::_thesis: q in A "\/" (B \/ C)
percases ( q in A "\/" B or q in A "\/" C ) by A3, XBOOLE_0:def_3;
suppose q in A "\/" B ; ::_thesis: q in A "\/" (B \/ C)
then consider a, b being Element of L such that
A4: ( q = a "\/" b & a in A ) and
A5: b in B ;
 b in B \/ C by A5, XBOOLE_0:def_3;
hence  q in A "\/" (B \/ C) by A4; ::_thesis: verum
end;
suppose q in A "\/" C ; ::_thesis: q in A "\/" (B \/ C)
then consider a, b being Element of L such that
A6: ( q = a "\/" b & a in A ) and
A7: b in C ;
 b in B \/ C by A7, XBOOLE_0:def_3;
hence  q in A "\/" (B \/ C) by A6; ::_thesis: verum
end;
end;
end;

theorem :: YELLOW_4:17
for L being reflexive antisymmetric with_suprema RelStr
for A, B, C being Subset of L holds A \/ (B "\/" C) c= (A \/ B) "\/" (A \/ C)
proof
let L be reflexive antisymmetric with_suprema RelStr ; ::_thesis: for A, B, C being Subset of L holds A \/ (B "\/" C) c= (A \/ B) "\/" (A \/ C)
let A, B, C be Subset of L; ::_thesis: A \/ (B "\/" C) c= (A \/ B) "\/" (A \/ C)
let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in A \/ (B "\/" C) or q in (A \/ B) "\/" (A \/ C) )
assume A1: q in A \/ (B "\/" C) ; ::_thesis: q in (A \/ B) "\/" (A \/ C)
percases ( q in A or q in B "\/" C ) by A1, XBOOLE_0:def_3;
supposeA2: q in A ; ::_thesis: q in (A \/ B) "\/" (A \/ C)
then reconsider q1 = q as Element of L ;
 q1 <= q1 ;
then A3: q1 = q1 "\/" q1 by YELLOW_0:24;
 ( q1 in A \/ B & q1 in A \/ C ) by A2, XBOOLE_0:def_3;
hence  q in (A \/ B) "\/" (A \/ C) by A3; ::_thesis: verum
end;
suppose q in B "\/" C ; ::_thesis: q in (A \/ B) "\/" (A \/ C)
then consider b, c being Element of L such that
A4: q = b "\/" c and
A5: ( b in B & c in C ) ;
 ( b in A \/ B & c in A \/ C ) by A5, XBOOLE_0:def_3;
hence  q in (A \/ B) "\/" (A \/ C) by A4; ::_thesis: verum
end;
end;
end;

theorem :: YELLOW_4:18
for L being antisymmetric with_suprema RelStr
for A being upper Subset of L
for B, C being Subset of L holds (A \/ B) "\/" (A \/ C) c= A \/ (B "\/" C)
proof
let L be antisymmetric with_suprema RelStr ; ::_thesis: for A being upper Subset of L
for B, C being Subset of L holds (A \/ B) "\/" (A \/ C) c= A \/ (B "\/" C)
let A be upper Subset of L; ::_thesis: for B, C being Subset of L holds (A \/ B) "\/" (A \/ C) c= A \/ (B "\/" C)
let B, C be Subset of L; ::_thesis: (A \/ B) "\/" (A \/ C) c= A \/ (B "\/" C)
let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in (A \/ B) "\/" (A \/ C) or q in A \/ (B "\/" C) )
assume  q in (A \/ B) "\/" (A \/ C) ; ::_thesis: q in A \/ (B "\/" C)
then consider x, y being Element of L such that
A1: q = x "\/" y and
A2: ( x in A \/ B & y in A \/ C ) ;
A3: x <= x "\/" y by YELLOW_0:22;
A4: y <= x "\/" y by YELLOW_0:22;
percases ( ( x in A & y in A ) or ( x in A & y in C ) or ( x in B & y in A ) or ( x in B & y in C ) ) by A2, XBOOLE_0:def_3;
suppose ( x in A & y in A ) ; ::_thesis: q in A \/ (B "\/" C)
then  q in A by A1, A3, WAYBEL_0:def_20;
hence  q in A \/ (B "\/" C) by XBOOLE_0:def_3; ::_thesis: verum
end;
suppose ( x in A & y in C ) ; ::_thesis: q in A \/ (B "\/" C)
then  q in A by A1, A3, WAYBEL_0:def_20;
hence  q in A \/ (B "\/" C) by XBOOLE_0:def_3; ::_thesis: verum
end;
suppose ( x in B & y in A ) ; ::_thesis: q in A \/ (B "\/" C)
then  q in A by A1, A4, WAYBEL_0:def_20;
hence  q in A \/ (B "\/" C) by XBOOLE_0:def_3; ::_thesis: verum
end;
suppose ( x in B & y in C ) ; ::_thesis: q in A \/ (B "\/" C)
then  x "\/" y in B "\/" C ;
hence  q in A \/ (B "\/" C) by A1, XBOOLE_0:def_3; ::_thesis: verum
end;
end;
end;

Lm1: now__::_thesis:_for_L_being_non_empty_RelStr_
for_x,_y_being_Element_of_L_holds__{__(a_"\/"_b)_where_a,_b_is_Element_of_L_:_(_a_in_{x}_&_b_in_{y}_)__}__=_{(x_"\/"_y)}
let L be non empty RelStr ; ::_thesis: for x, y being Element of L holds  {  (a "\/" b) where a, b is Element of L : ( a in {x} & b in {y} )  }  = {(x "\/" y)}
let x, y be Element of L; ::_thesis:  {  (a "\/" b) where a, b is Element of L : ( a in {x} & b in {y} )  }  = {(x "\/" y)}
thus   {  (a "\/" b) where a, b is Element of L : ( a in {x} & b in {y} )  }  = {(x "\/" y)} ::_thesis: verum
proof
thus   {  (a "\/" b) where a, b is Element of L : ( a in {x} & b in {y} )  }  c= {(x "\/" y)} :: according to XBOOLE_0:def_10 ::_thesis: {(x "\/" y)} c=  {  (a "\/" b) where a, b is Element of L : ( a in {x} & b in {y} )  }
proof
let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in  {  (a "\/" b) where a, b is Element of L : ( a in {x} & b in {y} )  }  or q in {(x "\/" y)} )
assume  q in  {  (a "\/" b) where a, b is Element of L : ( a in {x} & b in {y} )  }  ; ::_thesis: q in {(x "\/" y)}
then consider u, v being Element of L such that
A1: q = u "\/" v and
A2: ( u in {x} & v in {y} ) ;
 ( u = x & v = y ) by A2, TARSKI:def_1;
hence  q in {(x "\/" y)} by A1, TARSKI:def_1; ::_thesis: verum
end;
let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in {(x "\/" y)} or q in  {  (a "\/" b) where a, b is Element of L : ( a in {x} & b in {y} )  }  )
assume  q in {(x "\/" y)} ; ::_thesis: q in  {  (a "\/" b) where a, b is Element of L : ( a in {x} & b in {y} )  }
then A3: q = x "\/" y by TARSKI:def_1;
 ( x in {x} & y in {y} ) by TARSKI:def_1;
hence  q in  {  (a "\/" b) where a, b is Element of L : ( a in {x} & b in {y} )  }  by A3; ::_thesis: verum
end;
end;

Lm2: now__::_thesis:_for_L_being_non_empty_RelStr_
for_x,_y,_z_being_Element_of_L_holds__{__(a_"\/"_b)_where_a,_b_is_Element_of_L_:_(_a_in_{x}_&_b_in_{y,z}_)__}__=_{(x_"\/"_y),(x_"\/"_z)}
let L be non empty RelStr ; ::_thesis: for x, y, z being Element of L holds  {  (a "\/" b) where a, b is Element of L : ( a in {x} & b in {y,z} )  }  = {(x "\/" y),(x "\/" z)}
let x, y, z be Element of L; ::_thesis:  {  (a "\/" b) where a, b is Element of L : ( a in {x} & b in {y,z} )  }  = {(x "\/" y),(x "\/" z)}
thus   {  (a "\/" b) where a, b is Element of L : ( a in {x} & b in {y,z} )  }  = {(x "\/" y),(x "\/" z)} ::_thesis: verum
proof
thus   {  (a "\/" b) where a, b is Element of L : ( a in {x} & b in {y,z} )  }  c= {(x "\/" y),(x "\/" z)} :: according to XBOOLE_0:def_10 ::_thesis: {(x "\/" y),(x "\/" z)} c=  {  (a "\/" b) where a, b is Element of L : ( a in {x} & b in {y,z} )  }
proof
let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in  {  (a "\/" b) where a, b is Element of L : ( a in {x} & b in {y,z} )  }  or q in {(x "\/" y),(x "\/" z)} )
assume  q in  {  (a "\/" b) where a, b is Element of L : ( a in {x} & b in {y,z} )  }  ; ::_thesis: q in {(x "\/" y),(x "\/" z)}
then consider u, v being Element of L such that
A1: q = u "\/" v and
A2: u in {x} and
A3: v in {y,z} ;
A4: ( v = y or v = z ) by A3, TARSKI:def_2;
 u = x by A2, TARSKI:def_1;
hence  q in {(x "\/" y),(x "\/" z)} by A1, A4, TARSKI:def_2; ::_thesis: verum
end;
let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in {(x "\/" y),(x "\/" z)} or q in  {  (a "\/" b) where a, b is Element of L : ( a in {x} & b in {y,z} )  }  )
A5: z in {y,z} by TARSKI:def_2;
assume  q in {(x "\/" y),(x "\/" z)} ; ::_thesis: q in  {  (a "\/" b) where a, b is Element of L : ( a in {x} & b in {y,z} )  }
then A6: ( q = x "\/" y or q = x "\/" z ) by TARSKI:def_2;
 ( x in {x} & y in {y,z} ) by TARSKI:def_1, TARSKI:def_2;
hence  q in  {  (a "\/" b) where a, b is Element of L : ( a in {x} & b in {y,z} )  }  by A6, A5; ::_thesis: verum
end;
end;

theorem :: YELLOW_4:19
for L being non empty RelStr
for x, y being Element of L holds {x} "\/" {y} = {(x "\/" y)} by Lm1;

theorem :: YELLOW_4:20
for L being non empty RelStr
for x, y, z being Element of L holds {x} "\/" {y,z} = {(x "\/" y),(x "\/" z)} by Lm2;

theorem :: YELLOW_4:21
for L being non empty RelStr
for X1, X2, Y1, Y2 being Subset of L st X1 c= Y1 & X2 c= Y2 holds
X1 "\/" X2 c= Y1 "\/" Y2
proof
let L be non empty RelStr ; ::_thesis: for X1, X2, Y1, Y2 being Subset of L st X1 c= Y1 & X2 c= Y2 holds
X1 "\/" X2 c= Y1 "\/" Y2
let X1, X2, Y1, Y2 be Subset of L; ::_thesis: ( X1 c= Y1 & X2 c= Y2 implies X1 "\/" X2 c= Y1 "\/" Y2 )
assume A1: ( X1 c= Y1 & X2 c= Y2 ) ; ::_thesis: X1 "\/" X2 c= Y1 "\/" Y2
let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in X1 "\/" X2 or q in Y1 "\/" Y2 )
assume  q in X1 "\/" X2 ; ::_thesis: q in Y1 "\/" Y2
then  ex x, y being Element of L st
( q = x "\/" y & x in X1 & y in X2 ) ;
hence  q in Y1 "\/" Y2 by A1; ::_thesis: verum
end;

theorem :: YELLOW_4:22
for L being reflexive antisymmetric with_suprema RelStr
for D being Subset of L
for x being Element of L st x is_<=_than D holds
{x} "\/" D = D
proof
let L be reflexive antisymmetric with_suprema RelStr ; ::_thesis: for D being Subset of L
for x being Element of L st x is_<=_than D holds
{x} "\/" D = D
let D be Subset of L; ::_thesis: for x being Element of L st x is_<=_than D holds
{x} "\/" D = D
let x be Element of L; ::_thesis: ( x is_<=_than D implies {x} "\/" D = D )
assume A1: x is_<=_than D ; ::_thesis: {x} "\/" D = D
A2: {x} "\/" D =  {  (x "\/" y) where y is Element of L : y in D  }  by Th15;
thus  {x} "\/" D c= D :: according to XBOOLE_0:def_10 ::_thesis: D c= {x} "\/" D
proof
let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in {x} "\/" D or q in D )
assume  q in {x} "\/" D ; ::_thesis: q in D
then consider y being Element of L such that
A3: q = x "\/" y and
A4: y in D by A2;
 x <= y by A1, A4, LATTICE3:def_8;
hence  q in D by A3, A4, YELLOW_0:24; ::_thesis: verum
end;
let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in D or q in {x} "\/" D )
assume A5: q in D ; ::_thesis: q in {x} "\/" D
then reconsider D1 = D as non empty Subset of L ;
reconsider y = q as Element of D1 by A5;
 x <= y by A1, LATTICE3:def_8;
then  q = x "\/" y by YELLOW_0:24;
hence  q in {x} "\/" D by A2; ::_thesis: verum
end;

theorem :: YELLOW_4:23
for L being antisymmetric with_suprema RelStr
for D being Subset of L
for x being Element of L holds x is_<=_than {x} "\/" D
proof
let L be antisymmetric with_suprema RelStr ; ::_thesis: for D being Subset of L
for x being Element of L holds x is_<=_than {x} "\/" D
let D be Subset of L; ::_thesis: for x being Element of L holds x is_<=_than {x} "\/" D
let x be Element of L; ::_thesis: x is_<=_than {x} "\/" D
let b be Element of L; :: according to LATTICE3:def_8 ::_thesis: ( not b in {x} "\/" D or x <= b )
A1: {x} "\/" D =  {  (x "\/" h) where h is Element of L : h in D  }  by Th15;
assume  b in {x} "\/" D ; ::_thesis: x <= b
then consider h being Element of L such that
A2: b = x "\/" h and
 h in D by A1;
 ex w being Element of L st
( x <= w & h <= w & ( for c being Element of L st x <= c & h <= c holds
w <= c ) ) by LATTICE3:def_10;
hence  x <= b by A2, LATTICE3:def_13; ::_thesis: verum
end;

theorem :: YELLOW_4:24
for L being with_suprema Poset
for X being Subset of L
for x being Element of L st ex_inf_of {x} "\/" X,L & ex_inf_of X,L holds
x "\/" (inf X) <= inf ({x} "\/" X)
proof
let L be with_suprema Poset; ::_thesis: for X being Subset of L
for x being Element of L st ex_inf_of {x} "\/" X,L & ex_inf_of X,L holds
x "\/" (inf X) <= inf ({x} "\/" X)
let X be Subset of L; ::_thesis: for x being Element of L st ex_inf_of {x} "\/" X,L & ex_inf_of X,L holds
x "\/" (inf X) <= inf ({x} "\/" X)
let x be Element of L; ::_thesis: ( ex_inf_of {x} "\/" X,L & ex_inf_of X,L implies x "\/" (inf X) <= inf ({x} "\/" X) )
assume that
A1: ex_inf_of {x} "\/" X,L and
A2: ex_inf_of X,L ; ::_thesis: x "\/" (inf X) <= inf ({x} "\/" X)
A3: {x} "\/" X =  {  (x "\/" y) where y is Element of L : y in X  }  by Th15;
 {x} "\/" X is_>=_than x "\/" (inf X)
proof
let q be Element of L; :: according to LATTICE3:def_8 ::_thesis: ( not q in {x} "\/" X or x "\/" (inf X) <= q )
assume  q in {x} "\/" X ; ::_thesis: x "\/" (inf X) <= q
then consider y being Element of L such that
A4: q = x "\/" y and
A5: y in X by A3;
 ( x <= x & y >= inf X ) by A2, A5, Th2;
hence  x "\/" (inf X) <= q by A4, YELLOW_3:3; ::_thesis: verum
end;
hence  x "\/" (inf X) <= inf ({x} "\/" X) by A1, YELLOW_0:def_10; ::_thesis: verum
end;

theorem Th25: :: YELLOW_4:25
for L being non empty transitive antisymmetric complete RelStr
for A being Subset of L
for B being non empty Subset of L holds A is_<=_than sup (A "\/" B)
proof
let L be non empty transitive antisymmetric complete RelStr ; ::_thesis: for A being Subset of L
for B being non empty Subset of L holds A is_<=_than sup (A "\/" B)
let A be Subset of L; ::_thesis: for B being non empty Subset of L holds A is_<=_than sup (A "\/" B)
let B be non empty Subset of L; ::_thesis: A is_<=_than sup (A "\/" B)
set b = the Element of B;
let x be Element of L; :: according to LATTICE3:def_9 ::_thesis: ( not x in A or x <= sup (A "\/" B) )
assume  x in A ; ::_thesis: x <= sup (A "\/" B)
then A1: x "\/" the Element of B in A "\/" B ;
 ex xx being Element of L st
( x <= xx & the Element of B <= xx & ( for c being Element of L st x <= c & the Element of B <= c holds
xx <= c ) ) by LATTICE3:def_10;
then A2: x <= x "\/" the Element of B by LATTICE3:def_13;
 ex_sup_of A "\/" B,L by YELLOW_0:17;
then  A "\/" B is_<=_than sup (A "\/" B) by YELLOW_0:def_9;
then  x "\/" the Element of B <= sup (A "\/" B) by A1, LATTICE3:def_9;
hence  x <= sup (A "\/" B) by A2, YELLOW_0:def_2; ::_thesis: verum
end;

theorem :: YELLOW_4:26
for L being transitive antisymmetric with_suprema RelStr
for a, b being Element of L
for A, B being Subset of L st a is_<=_than A & b is_<=_than B holds
a "\/" b is_<=_than A "\/" B
proof
let L be transitive antisymmetric with_suprema RelStr ; ::_thesis: for a, b being Element of L
for A, B being Subset of L st a is_<=_than A & b is_<=_than B holds
a "\/" b is_<=_than A "\/" B
let a, b be Element of L; ::_thesis: for A, B being Subset of L st a is_<=_than A & b is_<=_than B holds
a "\/" b is_<=_than A "\/" B
let A, B be Subset of L; ::_thesis: ( a is_<=_than A & b is_<=_than B implies a "\/" b is_<=_than A "\/" B )
assume A1: ( a is_<=_than A & b is_<=_than B ) ; ::_thesis: a "\/" b is_<=_than A "\/" B
let q be Element of L; :: according to LATTICE3:def_8 ::_thesis: ( not q in A "\/" B or a "\/" b <= q )
assume  q in A "\/" B ; ::_thesis: a "\/" b <= q
then consider x, y being Element of L such that
A2: q = x "\/" y and
A3: ( x in A & y in B ) ;
 ( a <= x & b <= y ) by A1, A3, LATTICE3:def_8;
hence  a "\/" b <= q by A2, YELLOW_3:3; ::_thesis: verum
end;

theorem Th27: :: YELLOW_4:27
for L being transitive antisymmetric with_suprema RelStr
for a, b being Element of L
for A, B being Subset of L st a is_>=_than A & b is_>=_than B holds
a "\/" b is_>=_than A "\/" B
proof
let L be transitive antisymmetric with_suprema RelStr ; ::_thesis: for a, b being Element of L
for A, B being Subset of L st a is_>=_than A & b is_>=_than B holds
a "\/" b is_>=_than A "\/" B
let a, b be Element of L; ::_thesis: for A, B being Subset of L st a is_>=_than A & b is_>=_than B holds
a "\/" b is_>=_than A "\/" B
let A, B be Subset of L; ::_thesis: ( a is_>=_than A & b is_>=_than B implies a "\/" b is_>=_than A "\/" B )
assume A1: ( a is_>=_than A & b is_>=_than B ) ; ::_thesis: a "\/" b is_>=_than A "\/" B
let q be Element of L; :: according to LATTICE3:def_9 ::_thesis: ( not q in A "\/" B or q <= a "\/" b )
assume  q in A "\/" B ; ::_thesis: q <= a "\/" b
then consider x, y being Element of L such that
A2: q = x "\/" y and
A3: ( x in A & y in B ) ;
 ( a >= x & b >= y ) by A1, A3, LATTICE3:def_9;
hence  q <= a "\/" b by A2, YELLOW_3:3; ::_thesis: verum
end;

theorem :: YELLOW_4:28
for L being non empty complete Poset
for A, B being non empty Subset of L holds sup (A "\/" B) = (sup A) "\/" (sup B)
proof
let L be non empty complete Poset; ::_thesis: for A, B being non empty Subset of L holds sup (A "\/" B) = (sup A) "\/" (sup B)
let A, B be non empty Subset of L; ::_thesis: sup (A "\/" B) = (sup A) "\/" (sup B)
 B is_<=_than sup (A "\/" B) by Th25;
then A1: sup B <= sup (A "\/" B) by YELLOW_0:32;
 A is_<=_than sup (A "\/" B) by Th25;
then  sup A <= sup (A "\/" B) by YELLOW_0:32;
then A2: (sup A) "\/" (sup B) <= (sup (A "\/" B)) "\/" (sup (A "\/" B)) by A1, YELLOW_3:3;
 ( A is_<=_than sup A & B is_<=_than sup B ) by YELLOW_0:32;
then  ( ex_sup_of A "\/" B,L & A "\/" B is_<=_than (sup A) "\/" (sup B) ) by Th27, YELLOW_0:17;
then A3: sup (A "\/" B) <= (sup A) "\/" (sup B) by YELLOW_0:def_9;
 sup (A "\/" B) <= sup (A "\/" B) ;
then  (sup (A "\/" B)) "\/" (sup (A "\/" B)) = sup (A "\/" B) by YELLOW_0:24;
hence  sup (A "\/" B) = (sup A) "\/" (sup B) by A3, A2, ORDERS_2:2; ::_thesis: verum
end;

theorem Th29: :: YELLOW_4:29
for L being antisymmetric with_suprema RelStr
for X being Subset of L
for Y being non empty Subset of L holds X c= downarrow (X "\/" Y)
proof
let L be antisymmetric with_suprema RelStr ; ::_thesis: for X being Subset of L
for Y being non empty Subset of L holds X c= downarrow (X "\/" Y)
let X be Subset of L; ::_thesis: for Y being non empty Subset of L holds X c= downarrow (X "\/" Y)
let Y be non empty Subset of L; ::_thesis: X c= downarrow (X "\/" Y)
consider y being set  such that
A1: y in Y by XBOOLE_0:def_1;
reconsider y = y as Element of Y by A1;
let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in X or q in downarrow (X "\/" Y) )
assume A2: q in X ; ::_thesis: q in downarrow (X "\/" Y)
then reconsider X1 = X as non empty Subset of L ;
reconsider x = q as Element of X1 by A2;
 ex s being Element of L st
( x <= s & y <= s & ( for c being Element of L st x <= c & y <= c holds
s <= c ) ) by LATTICE3:def_10;
then A3: x <= x "\/" y by LATTICE3:def_13;
 ( downarrow (X "\/" Y) =  {  s where s is Element of L : ex y being Element of L st
( s <= y & y in X "\/" Y )  }  & x "\/" y in X1 "\/" Y ) by WAYBEL_0:14;
hence  q in downarrow (X "\/" Y) by A3; ::_thesis: verum
end;

theorem :: YELLOW_4:30
for L being with_suprema Poset
for x, y being Element of (InclPoset (Ids L))
for X, Y being Subset of L st x = X & y = Y holds
x "\/" y = downarrow (X "\/" Y)
proof
let L be with_suprema Poset; ::_thesis: for x, y being Element of (InclPoset (Ids L))
for X, Y being Subset of L st x = X & y = Y holds
x "\/" y = downarrow (X "\/" Y)
let x, y be Element of (InclPoset (Ids L)); ::_thesis: for X, Y being Subset of L st x = X & y = Y holds
x "\/" y = downarrow (X "\/" Y)
let X, Y be Subset of L; ::_thesis: ( x = X & y = Y implies x "\/" y = downarrow (X "\/" Y) )
assume that
A1: x = X and
A2: y = Y ; ::_thesis: x "\/" y = downarrow (X "\/" Y)
reconsider X1 = X, Y1 = Y as non empty directed Subset of L by A1, A2, YELLOW_2:41;
reconsider d = downarrow (X1 "\/" Y1) as Element of (InclPoset (Ids L)) by YELLOW_2:41;
 Y c= d by Th29;
then A3: y <= d by A2, YELLOW_1:3;
 X c= d by Th29;
then  x <= d by A1, YELLOW_1:3;
then  ( d <= d & x "\/" y <= d "\/" d ) by A3, YELLOW_3:3;
then  x "\/" y <= d by YELLOW_0:24;
hence  x "\/" y c= downarrow (X "\/" Y) by YELLOW_1:3; :: according to XBOOLE_0:def_10 ::_thesis: downarrow (X "\/" Y) c= x "\/" y
consider Z being Subset of L such that
A4: Z =  {  z where z is Element of L : ( z in x or z in y or ex a, b being Element of L st
( a in x & b in y & z = a "\/" b ) )  }  and
 ex_sup_of {x,y}, InclPoset (Ids L) and
A5: x "\/" y = downarrow Z by YELLOW_2:44;
 X "\/" Y c= Z
proof
let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in X "\/" Y or q in Z )
assume  q in X "\/" Y ; ::_thesis: q in Z
then  ex s, t being Element of L st
( q = s "\/" t & s in X & t in Y ) ;
hence  q in Z by A1, A2, A4; ::_thesis: verum
end;
hence  downarrow (X "\/" Y) c= x "\/" y by A5, YELLOW_3:6; ::_thesis: verum
end;

theorem :: YELLOW_4:31
for L being non empty RelStr
for D being Subset of [:L,L:] holds union  {  X where X is Subset of L : ex x being Element of L st
( X = {x} "\/" (proj2 D) & x in proj1 D )  }  = (proj1 D) "\/" (proj2 D)
proof
let L be non empty RelStr ; ::_thesis: for D being Subset of [:L,L:] holds union  {  X where X is Subset of L : ex x being Element of L st
( X = {x} "\/" (proj2 D) & x in proj1 D )  }  = (proj1 D) "\/" (proj2 D)
let D be Subset of [:L,L:]; ::_thesis: union  {  X where X is Subset of L : ex x being Element of L st
( X = {x} "\/" (proj2 D) & x in proj1 D )  }  = (proj1 D) "\/" (proj2 D)
set D1 = proj1 D;
set D2 = proj2 D;
defpred S1[ set ] means  ex x being Element of L st
( $1 = {x} "\/" (proj2 D) & x in proj1 D );
thus  union  {  X where X is Subset of L : S1[X]  }  c= (proj1 D) "\/" (proj2 D) :: according to XBOOLE_0:def_10 ::_thesis: (proj1 D) "\/" (proj2 D) c= union  {  X where X is Subset of L : ex x being Element of L st
( X = {x} "\/" (proj2 D) & x in proj1 D )  }
proof
let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in union  {  X where X is Subset of L : S1[X]  }  or q in (proj1 D) "\/" (proj2 D) )
assume  q in union  {  X where X is Subset of L : S1[X]  }  ; ::_thesis: q in (proj1 D) "\/" (proj2 D)
then consider w being set  such that
A1: q in w and
A2: w in  {  X where X is Subset of L : S1[X]  }  by TARSKI:def_4;
consider e being Subset of L such that
A3: w = e and
A4: S1[e] by A2;
consider p being Element of L such that
A5: e = {p} "\/" (proj2 D) and
A6: p in proj1 D by A4;
 {p} "\/" (proj2 D) =  {  (p "\/" y) where y is Element of L : y in proj2 D  }  by Th15;
then  ex y being Element of L st
( q = p "\/" y & y in proj2 D ) by A1, A3, A5;
hence  q in (proj1 D) "\/" (proj2 D) by A6; ::_thesis: verum
end;
let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in (proj1 D) "\/" (proj2 D) or q in union  {  X where X is Subset of L : ex x being Element of L st
( X = {x} "\/" (proj2 D) & x in proj1 D )  }  )
assume  q in (proj1 D) "\/" (proj2 D) ; ::_thesis: q in union  {  X where X is Subset of L : ex x being Element of L st
( X = {x} "\/" (proj2 D) & x in proj1 D )  }
then consider x, y being Element of L such that
A7: q = x "\/" y and
A8: x in proj1 D and
A9: y in proj2 D ;
 {x} "\/" (proj2 D) =  {  (x "\/" d) where d is Element of L : d in proj2 D  }  by Th15;
then A10: q in {x} "\/" (proj2 D) by A7, A9;
 {x} "\/" (proj2 D) in  {  X where X is Subset of L : S1[X]  }  by A8;
hence  q in union  {  X where X is Subset of L : ex x being Element of L st
( X = {x} "\/" (proj2 D) & x in proj1 D )  }  by A10, TARSKI:def_4; ::_thesis: verum
end;

theorem Th32: :: YELLOW_4:32
for L being transitive antisymmetric with_suprema RelStr
for D1, D2 being Subset of L holds downarrow ((downarrow D1) "\/" (downarrow D2)) c= downarrow (D1 "\/" D2)
proof
let L be transitive antisymmetric with_suprema RelStr ; ::_thesis: for D1, D2 being Subset of L holds downarrow ((downarrow D1) "\/" (downarrow D2)) c= downarrow (D1 "\/" D2)
let D1, D2 be Subset of L; ::_thesis: downarrow ((downarrow D1) "\/" (downarrow D2)) c= downarrow (D1 "\/" D2)
A1: downarrow ((downarrow D1) "\/" (downarrow D2)) =  {  x where x is Element of L : ex t being Element of L st
( x <= t & t in (downarrow D1) "\/" (downarrow D2) )  }  by WAYBEL_0:14;
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in downarrow ((downarrow D1) "\/" (downarrow D2)) or y in downarrow (D1 "\/" D2) )
assume  y in downarrow ((downarrow D1) "\/" (downarrow D2)) ; ::_thesis: y in downarrow (D1 "\/" D2)
then consider x being Element of L such that
A2: y = x and
A3: ex t being Element of L st
( x <= t & t in (downarrow D1) "\/" (downarrow D2) ) by A1;
consider x1 being Element of L such that
A4: x <= x1 and
A5: x1 in (downarrow D1) "\/" (downarrow D2) by A3;
consider a, b being Element of L such that
A6: x1 = a "\/" b and
A7: a in downarrow D1 and
A8: b in downarrow D2 by A5;
 downarrow D2 =  {  s2 where s2 is Element of L : ex z being Element of L st
( s2 <= z & z in D2 )  }  by WAYBEL_0:14;
then consider B1 being Element of L such that
A9: b = B1 and
A10: ex z being Element of L st
( B1 <= z & z in D2 ) by A8;
consider b1 being Element of L such that
A11: B1 <= b1 and
A12: b1 in D2 by A10;
 downarrow D1 =  {  s1 where s1 is Element of L : ex z being Element of L st
( s1 <= z & z in D1 )  }  by WAYBEL_0:14;
then consider A1 being Element of L such that
A13: a = A1 and
A14: ex z being Element of L st
( A1 <= z & z in D1 ) by A7;
consider a1 being Element of L such that
A15: A1 <= a1 and
A16: a1 in D1 by A14;
 x1 <= a1 "\/" b1 by A6, A13, A9, A15, A11, YELLOW_3:3;
then A17: ( downarrow (D1 "\/" D2) =  {  s where s is Element of L : ex z being Element of L st
( s <= z & z in D1 "\/" D2 )  }  & x <= a1 "\/" b1 ) by A4, ORDERS_2:3, WAYBEL_0:14;
 a1 "\/" b1 in D1 "\/" D2 by A16, A12;
hence  y in downarrow (D1 "\/" D2) by A2, A17; ::_thesis: verum
end;

theorem :: YELLOW_4:33
for L being with_suprema Poset
for D1, D2 being Subset of L holds downarrow ((downarrow D1) "\/" (downarrow D2)) = downarrow (D1 "\/" D2)
proof
let L be with_suprema Poset; ::_thesis: for D1, D2 being Subset of L holds downarrow ((downarrow D1) "\/" (downarrow D2)) = downarrow (D1 "\/" D2)
let D1, D2 be Subset of L; ::_thesis: downarrow ((downarrow D1) "\/" (downarrow D2)) = downarrow (D1 "\/" D2)
A1: downarrow (D1 "\/" D2) =  {  s where s is Element of L : ex z being Element of L st
( s <= z & z in D1 "\/" D2 )  }  by WAYBEL_0:14;
thus  downarrow ((downarrow D1) "\/" (downarrow D2)) c= downarrow (D1 "\/" D2) by Th32; :: according to XBOOLE_0:def_10 ::_thesis: downarrow (D1 "\/" D2) c= downarrow ((downarrow D1) "\/" (downarrow D2))
let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in downarrow (D1 "\/" D2) or q in downarrow ((downarrow D1) "\/" (downarrow D2)) )
assume  q in downarrow (D1 "\/" D2) ; ::_thesis: q in downarrow ((downarrow D1) "\/" (downarrow D2))
then consider s being Element of L such that
A2: q = s and
A3: ex z being Element of L st
( s <= z & z in D1 "\/" D2 ) by A1;
A4: downarrow ((downarrow D1) "\/" (downarrow D2)) =  {  x where x is Element of L : ex t being Element of L st
( x <= t & t in (downarrow D1) "\/" (downarrow D2) )  }  by WAYBEL_0:14;
A5: ( D1 is Subset of (downarrow D1) & D2 is Subset of (downarrow D2) ) by WAYBEL_0:16;
consider x being Element of L such that
A6: s <= x and
A7: x in D1 "\/" D2 by A3;
 ex a, b being Element of L st
( x = a "\/" b & a in D1 & b in D2 ) by A7;
then  x in (downarrow D1) "\/" (downarrow D2) by A5;
hence  q in downarrow ((downarrow D1) "\/" (downarrow D2)) by A4, A2, A6; ::_thesis: verum
end;

theorem Th34: :: YELLOW_4:34
for L being transitive antisymmetric with_suprema RelStr
for D1, D2 being Subset of L holds uparrow ((uparrow D1) "\/" (uparrow D2)) c= uparrow (D1 "\/" D2)
proof
let L be transitive antisymmetric with_suprema RelStr ; ::_thesis: for D1, D2 being Subset of L holds uparrow ((uparrow D1) "\/" (uparrow D2)) c= uparrow (D1 "\/" D2)
let D1, D2 be Subset of L; ::_thesis: uparrow ((uparrow D1) "\/" (uparrow D2)) c= uparrow (D1 "\/" D2)
A1: uparrow ((uparrow D1) "\/" (uparrow D2)) =  {  x where x is Element of L : ex t being Element of L st
( x >= t & t in (uparrow D1) "\/" (uparrow D2) )  }  by WAYBEL_0:15;
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in uparrow ((uparrow D1) "\/" (uparrow D2)) or y in uparrow (D1 "\/" D2) )
assume  y in uparrow ((uparrow D1) "\/" (uparrow D2)) ; ::_thesis: y in uparrow (D1 "\/" D2)
then consider x being Element of L such that
A2: y = x and
A3: ex t being Element of L st
( x >= t & t in (uparrow D1) "\/" (uparrow D2) ) by A1;
consider x1 being Element of L such that
A4: x >= x1 and
A5: x1 in (uparrow D1) "\/" (uparrow D2) by A3;
consider a, b being Element of L such that
A6: x1 = a "\/" b and
A7: a in uparrow D1 and
A8: b in uparrow D2 by A5;
 uparrow D2 =  {  s2 where s2 is Element of L : ex z being Element of L st
( s2 >= z & z in D2 )  }  by WAYBEL_0:15;
then consider B1 being Element of L such that
A9: b = B1 and
A10: ex z being Element of L st
( B1 >= z & z in D2 ) by A8;
consider b1 being Element of L such that
A11: B1 >= b1 and
A12: b1 in D2 by A10;
 uparrow D1 =  {  s1 where s1 is Element of L : ex z being Element of L st
( s1 >= z & z in D1 )  }  by WAYBEL_0:15;
then consider A1 being Element of L such that
A13: a = A1 and
A14: ex z being Element of L st
( A1 >= z & z in D1 ) by A7;
consider a1 being Element of L such that
A15: A1 >= a1 and
A16: a1 in D1 by A14;
 x1 >= a1 "\/" b1 by A6, A13, A9, A15, A11, YELLOW_3:3;
then A17: ( uparrow (D1 "\/" D2) =  {  s where s is Element of L : ex z being Element of L st
( s >= z & z in D1 "\/" D2 )  }  & x >= a1 "\/" b1 ) by A4, ORDERS_2:3, WAYBEL_0:15;
 a1 "\/" b1 in D1 "\/" D2 by A16, A12;
hence  y in uparrow (D1 "\/" D2) by A2, A17; ::_thesis: verum
end;

theorem :: YELLOW_4:35
for L being with_suprema Poset
for D1, D2 being Subset of L holds uparrow ((uparrow D1) "\/" (uparrow D2)) = uparrow (D1 "\/" D2)
proof
let L be with_suprema Poset; ::_thesis: for D1, D2 being Subset of L holds uparrow ((uparrow D1) "\/" (uparrow D2)) = uparrow (D1 "\/" D2)
let D1, D2 be Subset of L; ::_thesis: uparrow ((uparrow D1) "\/" (uparrow D2)) = uparrow (D1 "\/" D2)
A1: uparrow (D1 "\/" D2) =  {  s where s is Element of L : ex z being Element of L st
( s >= z & z in D1 "\/" D2 )  }  by WAYBEL_0:15;
thus  uparrow ((uparrow D1) "\/" (uparrow D2)) c= uparrow (D1 "\/" D2) by Th34; :: according to XBOOLE_0:def_10 ::_thesis: uparrow (D1 "\/" D2) c= uparrow ((uparrow D1) "\/" (uparrow D2))
let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in uparrow (D1 "\/" D2) or q in uparrow ((uparrow D1) "\/" (uparrow D2)) )
assume  q in uparrow (D1 "\/" D2) ; ::_thesis: q in uparrow ((uparrow D1) "\/" (uparrow D2))
then consider s being Element of L such that
A2: q = s and
A3: ex z being Element of L st
( s >= z & z in D1 "\/" D2 ) by A1;
A4: uparrow ((uparrow D1) "\/" (uparrow D2)) =  {  x where x is Element of L : ex t being Element of L st
( x >= t & t in (uparrow D1) "\/" (uparrow D2) )  }  by WAYBEL_0:15;
A5: ( D1 is Subset of (uparrow D1) & D2 is Subset of (uparrow D2) ) by WAYBEL_0:16;
consider x being Element of L such that
A6: s >= x and
A7: x in D1 "\/" D2 by A3;
 ex a, b being Element of L st
( x = a "\/" b & a in D1 & b in D2 ) by A7;
then  x in (uparrow D1) "\/" (uparrow D2) by A5;
hence  q in uparrow ((uparrow D1) "\/" (uparrow D2)) by A4, A2, A6; ::_thesis: verum
end;

begin

definition
let L be non empty RelStr ;
let D1, D2 be Subset of L;
funcD1 "/\" D2 ->  Subset of L equals :: YELLOW_4:def 4
 {  (x "/\" y) where x, y is Element of L : ( x in D1 & y in D2 )  }  ;
coherence
  {  (x "/\" y) where x, y is Element of L : ( x in D1 & y in D2 )  }  is Subset of L
proof
  {  (x "/\" y) where x, y is Element of L : ( x in D1 & y in D2 )  }  c= the carrier of L
proof
let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in  {  (x "/\" y) where x, y is Element of L : ( x in D1 & y in D2 )  }  or q in the carrier of L )
assume  q in  {  (x "/\" y) where x, y is Element of L : ( x in D1 & y in D2 )  }  ; ::_thesis: q in the carrier of L
then  ex a, b being Element of L st
( q = a "/\" b & a in D1 & b in D2 ) ;
hence  q in the carrier of L ; ::_thesis: verum
end;
hence   {  (x "/\" y) where x, y is Element of L : ( x in D1 & y in D2 )  }  is Subset of L ; ::_thesis: verum
end;
end;

:: deftheorem  defines "/\" YELLOW_4:def_4_:_
 for L being non empty RelStr
for D1, D2 being Subset of L holds D1 "/\" D2 =  {  (x "/\" y) where x, y is Element of L : ( x in D1 & y in D2 )  }  ;

definition
let L be antisymmetric with_infima RelStr ;
let D1, D2 be Subset of L;
:: original: "/\"
redefine funcD1 "/\" D2 ->  Subset of L;
commutativity
 for D1, D2 being Subset of L holds D1 "/\" D2 = D2 "/\" D1
proof
let D1, D2 be Subset of L; ::_thesis: D1 "/\" D2 = D2 "/\" D1
thus  D1 "/\" D2 c= D2 "/\" D1 :: according to XBOOLE_0:def_10 ::_thesis: D2 "/\" D1 c= D1 "/\" D2
proof
let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in D1 "/\" D2 or q in D2 "/\" D1 )
assume  q in D1 "/\" D2 ; ::_thesis: q in D2 "/\" D1
then  ex x, y being Element of L st
( q = x "/\" y & x in D1 & y in D2 ) ;
hence  q in D2 "/\" D1 ; ::_thesis: verum
end;
let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in D2 "/\" D1 or q in D1 "/\" D2 )
assume  q in D2 "/\" D1 ; ::_thesis: q in D1 "/\" D2
then  ex x, y being Element of L st
( q = x "/\" y & x in D2 & y in D1 ) ;
hence  q in D1 "/\" D2 ; ::_thesis: verum
end;
end;

theorem :: YELLOW_4:36
for L being non empty RelStr
for X being Subset of L holds X "/\" ({} L) = {}
proof
let L be non empty RelStr ; ::_thesis: for X being Subset of L holds X "/\" ({} L) = {}
let X be Subset of L; ::_thesis: X "/\" ({} L) = {}
thus  X "/\" ({} L) c= {} :: according to XBOOLE_0:def_10 ::_thesis: {} c= X "/\" ({} L)
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in X "/\" ({} L) or a in {} )
assume  a in X "/\" ({} L) ; ::_thesis: a in {}
then  ex s, t being Element of L st
( a = s "/\" t & s in X & t in {} L ) ;
hence  a in {} ; ::_thesis: verum
end;
thus  {} c= X "/\" ({} L) by XBOOLE_1:2; ::_thesis: verum
end;

theorem :: YELLOW_4:37
for L being non empty RelStr
for X, Y being Subset of L
for x, y being Element of L st x in X & y in Y holds
x "/\" y in X "/\" Y ;

theorem :: YELLOW_4:38
for L being antisymmetric with_infima RelStr
for A being Subset of L
for B being non empty Subset of L holds A is_coarser_than A "/\" B
proof
let L be antisymmetric with_infima RelStr ; ::_thesis: for A being Subset of L
for B being non empty Subset of L holds A is_coarser_than A "/\" B
let A be Subset of L; ::_thesis: for B being non empty Subset of L holds A is_coarser_than A "/\" B
let B be non empty Subset of L; ::_thesis: A is_coarser_than A "/\" B
consider b being set  such that
A1: b in B by XBOOLE_0:def_1;
reconsider b = b as Element of B by A1;
let q be Element of L; :: according to YELLOW_4:def_2 ::_thesis: ( q in A implies ex a being Element of L st
( a in A "/\" B & a <= q ) )
assume A2: q in A ; ::_thesis: ex a being Element of L st
( a in A "/\" B & a <= q )
take  q "/\" b ; ::_thesis: ( q "/\" b in A "/\" B & q "/\" b <= q )
thus  q "/\" b in A "/\" B by A2; ::_thesis: q "/\" b <= q
thus  q "/\" b <= q by YELLOW_0:23; ::_thesis: verum
end;

theorem :: YELLOW_4:39
for L being antisymmetric with_infima RelStr
for A, B being Subset of L holds A "/\" B is_finer_than A
proof
let L be antisymmetric with_infima RelStr ; ::_thesis: for A, B being Subset of L holds A "/\" B is_finer_than A
let A, B be Subset of L; ::_thesis: A "/\" B is_finer_than A
let q be Element of L; :: according to YELLOW_4:def_1 ::_thesis: ( q in A "/\" B implies ex b being Element of L st
( b in A & q <= b ) )
assume  q in A "/\" B ; ::_thesis: ex b being Element of L st
( b in A & q <= b )
then consider x, y being Element of L such that
A1: q = x "/\" y and
A2: x in A and
 y in B ;
take  x ; ::_thesis: ( x in A & q <= x )
thus  x in A by A2; ::_thesis: q <= x
thus  q <= x by A1, YELLOW_0:23; ::_thesis: verum
end;

theorem :: YELLOW_4:40
for L being reflexive antisymmetric with_infima RelStr
for A being Subset of L holds A c= A "/\" A
proof
let L be reflexive antisymmetric with_infima RelStr ; ::_thesis: for A being Subset of L holds A c= A "/\" A
let A be Subset of L; ::_thesis: A c= A "/\" A
let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in A or q in A "/\" A )
assume A1: q in A ; ::_thesis: q in A "/\" A
then reconsider A1 = A as non empty Subset of L ;
reconsider q1 = q as Element of A1 by A1;
 q1 = q1 "/\" q1 by YELLOW_0:25;
hence  q in A "/\" A ; ::_thesis: verum
end;

theorem :: YELLOW_4:41
for L being transitive antisymmetric with_infima RelStr
for D1, D2, D3 being Subset of L holds (D1 "/\" D2) "/\" D3 = D1 "/\" (D2 "/\" D3)
proof
let L be transitive antisymmetric with_infima RelStr ; ::_thesis: for D1, D2, D3 being Subset of L holds (D1 "/\" D2) "/\" D3 = D1 "/\" (D2 "/\" D3)
let D1, D2, D3 be Subset of L; ::_thesis: (D1 "/\" D2) "/\" D3 = D1 "/\" (D2 "/\" D3)
thus  (D1 "/\" D2) "/\" D3 c= D1 "/\" (D2 "/\" D3) :: according to XBOOLE_0:def_10 ::_thesis: D1 "/\" (D2 "/\" D3) c= (D1 "/\" D2) "/\" D3
proof
let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in (D1 "/\" D2) "/\" D3 or q in D1 "/\" (D2 "/\" D3) )
assume  q in (D1 "/\" D2) "/\" D3 ; ::_thesis: q in D1 "/\" (D2 "/\" D3)
then consider a1, b1 being Element of L such that
A1: q = a1 "/\" b1 and
A2: a1 in D1 "/\" D2 and
A3: b1 in D3 ;
consider a11, b11 being Element of L such that
A4: a1 = a11 "/\" b11 and
A5: a11 in D1 and
A6: b11 in D2 by A2;
 ( b11 "/\" b1 in D2 "/\" D3 & q = a11 "/\" (b11 "/\" b1) ) by A1, A3, A4, A6, LATTICE3:16;
hence  q in D1 "/\" (D2 "/\" D3) by A5; ::_thesis: verum
end;
let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in D1 "/\" (D2 "/\" D3) or q in (D1 "/\" D2) "/\" D3 )
assume  q in D1 "/\" (D2 "/\" D3) ; ::_thesis: q in (D1 "/\" D2) "/\" D3
then consider a1, b1 being Element of L such that
A7: ( q = a1 "/\" b1 & a1 in D1 ) and
A8: b1 in D2 "/\" D3 ;
consider a11, b11 being Element of L such that
A9: ( b1 = a11 "/\" b11 & a11 in D2 ) and
A10: b11 in D3 by A8;
 ( a1 "/\" a11 in D1 "/\" D2 & q = (a1 "/\" a11) "/\" b11 ) by A7, A9, LATTICE3:16;
hence  q in (D1 "/\" D2) "/\" D3 by A10; ::_thesis: verum
end;

registration
let L be non empty RelStr ;
let D1, D2 be non empty Subset of L;
clusterD1 "/\" D2 ->  non empty ;
coherence
 not D1 "/\" D2 is empty
proof
consider b being set  such that
A1: b in D2 by XBOOLE_0:def_1;
reconsider b = b as Element of D2 by A1;
consider a being set  such that
A2: a in D1 by XBOOLE_0:def_1;
reconsider a = a as Element of D1 by A2;
 a "/\" b in  {  (x "/\" y) where x, y is Element of L : ( x in D1 & y in D2 )  }  ;
hence  not D1 "/\" D2 is empty ; ::_thesis: verum
end;
end;

registration
let L be transitive antisymmetric with_infima RelStr ;
let D1, D2 be directed Subset of L;
clusterD1 "/\" D2 ->  directed ;
coherence
 D1 "/\" D2 is directed
proof
let a, b be Element of L; :: according to WAYBEL_0:def_1 ::_thesis: ( not a in D1 "/\" D2 or not b in D1 "/\" D2 or ex b1 being Element of the carrier of L st
( b1 in D1 "/\" D2 & a <= b1 & b <= b1 ) )
set X = D1 "/\" D2;
assume that
A1: a in D1 "/\" D2 and
A2: b in D1 "/\" D2 ; ::_thesis: ex b1 being Element of the carrier of L st
( b1 in D1 "/\" D2 & a <= b1 & b <= b1 )
consider x, y being Element of L such that
A3: a = x "/\" y and
A4: x in D1 and
A5: y in D2 by A1;
consider s, t being Element of L such that
A6: b = s "/\" t and
A7: s in D1 and
A8: t in D2 by A2;
consider z2 being Element of L such that
A9: z2 in D2 and
A10: ( y <= z2 & t <= z2 ) by A5, A8, WAYBEL_0:def_1;
consider z1 being Element of L such that
A11: z1 in D1 and
A12: ( x <= z1 & s <= z1 ) by A4, A7, WAYBEL_0:def_1;
take z = z1 "/\" z2; ::_thesis: ( z in D1 "/\" D2 & a <= z & b <= z )
thus  z in D1 "/\" D2 by A11, A9; ::_thesis: ( a <= z & b <= z )
thus  ( a <= z & b <= z ) by A3, A6, A12, A10, YELLOW_3:2; ::_thesis: verum
end;
end;

registration
let L be transitive antisymmetric with_infima RelStr ;
let D1, D2 be filtered Subset of L;
clusterD1 "/\" D2 ->  filtered ;
coherence
 D1 "/\" D2 is filtered
proof
let a, b be Element of L; :: according to WAYBEL_0:def_2 ::_thesis: ( not a in D1 "/\" D2 or not b in D1 "/\" D2 or ex b1 being Element of the carrier of L st
( b1 in D1 "/\" D2 & b1 <= a & b1 <= b ) )
set X = D1 "/\" D2;
assume that
A1: a in D1 "/\" D2 and
A2: b in D1 "/\" D2 ; ::_thesis: ex b1 being Element of the carrier of L st
( b1 in D1 "/\" D2 & b1 <= a & b1 <= b )
consider x, y being Element of L such that
A3: a = x "/\" y and
A4: x in D1 and
A5: y in D2 by A1;
consider s, t being Element of L such that
A6: b = s "/\" t and
A7: s in D1 and
A8: t in D2 by A2;
consider z2 being Element of L such that
A9: z2 in D2 and
A10: ( y >= z2 & t >= z2 ) by A5, A8, WAYBEL_0:def_2;
consider z1 being Element of L such that
A11: z1 in D1 and
A12: ( x >= z1 & s >= z1 ) by A4, A7, WAYBEL_0:def_2;
take z = z1 "/\" z2; ::_thesis: ( z in D1 "/\" D2 & z <= a & z <= b )
thus  z in D1 "/\" D2 by A11, A9; ::_thesis: ( z <= a & z <= b )
thus  ( z <= a & z <= b ) by A3, A6, A12, A10, YELLOW_3:2; ::_thesis: verum
end;
end;

registration
let L be Semilattice;
let D1, D2 be lower Subset of L;
clusterD1 "/\" D2 ->  lower ;
coherence
 D1 "/\" D2 is lower
proof
set X = D1 "/\" D2;
let a, b be Element of L; :: according to WAYBEL_0:def_19 ::_thesis: ( not a in D1 "/\" D2 or not b <= a or b in D1 "/\" D2 )
assume that
A1: a in D1 "/\" D2 and
A2: b <= a ; ::_thesis: b in D1 "/\" D2
consider x, y being Element of L such that
A3: a = x "/\" y and
A4: x in D1 and
A5: y in D2 by A1;
A6: ex xx being Element of L st
( x >= xx & y >= xx & ( for c being Element of L st x >= c & y >= c holds
xx >= c ) ) by LATTICE3:def_11;
then  x "/\" y <= x by LATTICE3:def_14;
then  b <= x by A2, A3, YELLOW_0:def_2;
then A7: b in D1 by A4, WAYBEL_0:def_19;
 x "/\" y <= y by A6, LATTICE3:def_14;
then  b <= y by A2, A3, YELLOW_0:def_2;
then A8: b in D2 by A5, WAYBEL_0:def_19;
 b = b "/\" b by YELLOW_0:25;
hence  b in D1 "/\" D2 by A7, A8; ::_thesis: verum
end;
end;

theorem Th42: :: YELLOW_4:42
for L being non empty RelStr
for Y being Subset of L
for x being Element of L holds {x} "/\" Y =  {  (x "/\" y) where y is Element of L : y in Y  }
proof
let L be non empty RelStr ; ::_thesis: for Y being Subset of L
for x being Element of L holds {x} "/\" Y =  {  (x "/\" y) where y is Element of L : y in Y  }
let Y be Subset of L; ::_thesis: for x being Element of L holds {x} "/\" Y =  {  (x "/\" y) where y is Element of L : y in Y  }
let x be Element of L; ::_thesis: {x} "/\" Y =  {  (x "/\" y) where y is Element of L : y in Y  }
thus  {x} "/\" Y c=  {  (x "/\" y) where y is Element of L : y in Y  }  :: according to XBOOLE_0:def_10 ::_thesis:  {  (x "/\" y) where y is Element of L : y in Y  }  c= {x} "/\" Y
proof
let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in {x} "/\" Y or q in  {  (x "/\" y) where y is Element of L : y in Y  }  )
assume  q in {x} "/\" Y ; ::_thesis: q in  {  (x "/\" y) where y is Element of L : y in Y  }
then consider s, t being Element of L such that
A1: q = s "/\" t and
A2: s in {x} and
A3: t in Y ;
 s = x by A2, TARSKI:def_1;
hence  q in  {  (x "/\" y) where y is Element of L : y in Y  }  by A1, A3; ::_thesis: verum
end;
let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in  {  (x "/\" y) where y is Element of L : y in Y  }  or q in {x} "/\" Y )
assume  q in  {  (x "/\" y) where y is Element of L : y in Y  }  ; ::_thesis: q in {x} "/\" Y
then A4: ex y being Element of L st
( q = x "/\" y & y in Y ) ;
 x in {x} by TARSKI:def_1;
hence  q in {x} "/\" Y by A4; ::_thesis: verum
end;

theorem :: YELLOW_4:43
for L being non empty RelStr
for A, B, C being Subset of L holds A "/\" (B \/ C) = (A "/\" B) \/ (A "/\" C)
proof
let L be non empty RelStr ; ::_thesis: for A, B, C being Subset of L holds A "/\" (B \/ C) = (A "/\" B) \/ (A "/\" C)
let A, B, C be Subset of L; ::_thesis: A "/\" (B \/ C) = (A "/\" B) \/ (A "/\" C)
thus  A "/\" (B \/ C) c= (A "/\" B) \/ (A "/\" C) :: according to XBOOLE_0:def_10 ::_thesis: (A "/\" B) \/ (A "/\" C) c= A "/\" (B \/ C)
proof
let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in A "/\" (B \/ C) or q in (A "/\" B) \/ (A "/\" C) )
assume  q in A "/\" (B \/ C) ; ::_thesis: q in (A "/\" B) \/ (A "/\" C)
then consider a, y being Element of L such that
A1: ( q = a "/\" y & a in A ) and
A2: y in B \/ C ;
 ( y in B or y in C ) by A2, XBOOLE_0:def_3;
then  ( q in A "/\" B or q in A "/\" C ) by A1;
hence  q in (A "/\" B) \/ (A "/\" C) by XBOOLE_0:def_3; ::_thesis: verum
end;
let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in (A "/\" B) \/ (A "/\" C) or q in A "/\" (B \/ C) )
assume A3: q in (A "/\" B) \/ (A "/\" C) ; ::_thesis: q in A "/\" (B \/ C)
percases ( q in A "/\" B or q in A "/\" C ) by A3, XBOOLE_0:def_3;
suppose q in A "/\" B ; ::_thesis: q in A "/\" (B \/ C)
then consider a, b being Element of L such that
A4: ( q = a "/\" b & a in A ) and
A5: b in B ;
 b in B \/ C by A5, XBOOLE_0:def_3;
hence  q in A "/\" (B \/ C) by A4; ::_thesis: verum
end;
suppose q in A "/\" C ; ::_thesis: q in A "/\" (B \/ C)
then consider a, b being Element of L such that
A6: ( q = a "/\" b & a in A ) and
A7: b in C ;
 b in B \/ C by A7, XBOOLE_0:def_3;
hence  q in A "/\" (B \/ C) by A6; ::_thesis: verum
end;
end;
end;

theorem :: YELLOW_4:44
for L being reflexive antisymmetric with_infima RelStr
for A, B, C being Subset of L holds A \/ (B "/\" C) c= (A \/ B) "/\" (A \/ C)
proof
let L be reflexive antisymmetric with_infima RelStr ; ::_thesis: for A, B, C being Subset of L holds A \/ (B "/\" C) c= (A \/ B) "/\" (A \/ C)
let A, B, C be Subset of L; ::_thesis: A \/ (B "/\" C) c= (A \/ B) "/\" (A \/ C)
let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in A \/ (B "/\" C) or q in (A \/ B) "/\" (A \/ C) )
assume A1: q in A \/ (B "/\" C) ; ::_thesis: q in (A \/ B) "/\" (A \/ C)
percases ( q in A or q in B "/\" C ) by A1, XBOOLE_0:def_3;
supposeA2: q in A ; ::_thesis: q in (A \/ B) "/\" (A \/ C)
then reconsider q1 = q as Element of L ;
A3: q1 = q1 "/\" q1 by YELLOW_0:25;
 ( q1 in A \/ B & q1 in A \/ C ) by A2, XBOOLE_0:def_3;
hence  q in (A \/ B) "/\" (A \/ C) by A3; ::_thesis: verum
end;
suppose q in B "/\" C ; ::_thesis: q in (A \/ B) "/\" (A \/ C)
then consider b, c being Element of L such that
A4: q = b "/\" c and
A5: ( b in B & c in C ) ;
 ( b in A \/ B & c in A \/ C ) by A5, XBOOLE_0:def_3;
hence  q in (A \/ B) "/\" (A \/ C) by A4; ::_thesis: verum
end;
end;
end;

theorem :: YELLOW_4:45
for L being antisymmetric with_infima RelStr
for A being lower Subset of L
for B, C being Subset of L holds (A \/ B) "/\" (A \/ C) c= A \/ (B "/\" C)
proof
let L be antisymmetric with_infima RelStr ; ::_thesis: for A being lower Subset of L
for B, C being Subset of L holds (A \/ B) "/\" (A \/ C) c= A \/ (B "/\" C)
let A be lower Subset of L; ::_thesis: for B, C being Subset of L holds (A \/ B) "/\" (A \/ C) c= A \/ (B "/\" C)
let B, C be Subset of L; ::_thesis: (A \/ B) "/\" (A \/ C) c= A \/ (B "/\" C)
let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in (A \/ B) "/\" (A \/ C) or q in A \/ (B "/\" C) )
assume  q in (A \/ B) "/\" (A \/ C) ; ::_thesis: q in A \/ (B "/\" C)
then consider x, y being Element of L such that
A1: q = x "/\" y and
A2: ( x in A \/ B & y in A \/ C ) ;
A3: x "/\" y <= x by YELLOW_0:23;
A4: x "/\" y <= y by YELLOW_0:23;
percases ( ( x in A & y in A ) or ( x in A & y in C ) or ( x in B & y in A ) or ( x in B & y in C ) ) by A2, XBOOLE_0:def_3;
suppose ( x in A & y in A ) ; ::_thesis: q in A \/ (B "/\" C)
then  q in A by A1, A3, WAYBEL_0:def_19;
hence  q in A \/ (B "/\" C) by XBOOLE_0:def_3; ::_thesis: verum
end;
suppose ( x in A & y in C ) ; ::_thesis: q in A \/ (B "/\" C)
then  q in A by A1, A3, WAYBEL_0:def_19;
hence  q in A \/ (B "/\" C) by XBOOLE_0:def_3; ::_thesis: verum
end;
suppose ( x in B & y in A ) ; ::_thesis: q in A \/ (B "/\" C)
then  q in A by A1, A4, WAYBEL_0:def_19;
hence  q in A \/ (B "/\" C) by XBOOLE_0:def_3; ::_thesis: verum
end;
suppose ( x in B & y in C ) ; ::_thesis: q in A \/ (B "/\" C)
then  x "/\" y in B "/\" C ;
hence  q in A \/ (B "/\" C) by A1, XBOOLE_0:def_3; ::_thesis: verum
end;
end;
end;

Lm3: now__::_thesis:_for_L_being_non_empty_RelStr_
for_x,_y_being_Element_of_L_holds__{__(a_"/\"_b)_where_a,_b_is_Element_of_L_:_(_a_in_{x}_&_b_in_{y}_)__}__=_{(x_"/\"_y)}
let L be non empty RelStr ; ::_thesis: for x, y being Element of L holds  {  (a "/\" b) where a, b is Element of L : ( a in {x} & b in {y} )  }  = {(x "/\" y)}
let x, y be Element of L; ::_thesis:  {  (a "/\" b) where a, b is Element of L : ( a in {x} & b in {y} )  }  = {(x "/\" y)}
thus   {  (a "/\" b) where a, b is Element of L : ( a in {x} & b in {y} )  }  = {(x "/\" y)} ::_thesis: verum
proof
thus   {  (a "/\" b) where a, b is Element of L : ( a in {x} & b in {y} )  }  c= {(x "/\" y)} :: according to XBOOLE_0:def_10 ::_thesis: {(x "/\" y)} c=  {  (a "/\" b) where a, b is Element of L : ( a in {x} & b in {y} )  }
proof
let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in  {  (a "/\" b) where a, b is Element of L : ( a in {x} & b in {y} )  }  or q in {(x "/\" y)} )
assume  q in  {  (a "/\" b) where a, b is Element of L : ( a in {x} & b in {y} )  }  ; ::_thesis: q in {(x "/\" y)}
then consider u, v being Element of L such that
A1: q = u "/\" v and
A2: ( u in {x} & v in {y} ) ;
 ( u = x & v = y ) by A2, TARSKI:def_1;
hence  q in {(x "/\" y)} by A1, TARSKI:def_1; ::_thesis: verum
end;
let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in {(x "/\" y)} or q in  {  (a "/\" b) where a, b is Element of L : ( a in {x} & b in {y} )  }  )
assume  q in {(x "/\" y)} ; ::_thesis: q in  {  (a "/\" b) where a, b is Element of L : ( a in {x} & b in {y} )  }
then A3: q = x "/\" y by TARSKI:def_1;
 ( x in {x} & y in {y} ) by TARSKI:def_1;
hence  q in  {  (a "/\" b) where a, b is Element of L : ( a in {x} & b in {y} )  }  by A3; ::_thesis: verum
end;
end;

Lm4: now__::_thesis:_for_L_being_non_empty_RelStr_
for_x,_y,_z_being_Element_of_L_holds__{__(a_"/\"_b)_where_a,_b_is_Element_of_L_:_(_a_in_{x}_&_b_in_{y,z}_)__}__=_{(x_"/\"_y),(x_"/\"_z)}
let L be non empty RelStr ; ::_thesis: for x, y, z being Element of L holds  {  (a "/\" b) where a, b is Element of L : ( a in {x} & b in {y,z} )  }  = {(x "/\" y),(x "/\" z)}
let x, y, z be Element of L; ::_thesis:  {  (a "/\" b) where a, b is Element of L : ( a in {x} & b in {y,z} )  }  = {(x "/\" y),(x "/\" z)}
thus   {  (a "/\" b) where a, b is Element of L : ( a in {x} & b in {y,z} )  }  = {(x "/\" y),(x "/\" z)} ::_thesis: verum
proof
thus   {  (a "/\" b) where a, b is Element of L : ( a in {x} & b in {y,z} )  }  c= {(x "/\" y),(x "/\" z)} :: according to XBOOLE_0:def_10 ::_thesis: {(x "/\" y),(x "/\" z)} c=  {  (a "/\" b) where a, b is Element of L : ( a in {x} & b in {y,z} )  }
proof
let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in  {  (a "/\" b) where a, b is Element of L : ( a in {x} & b in {y,z} )  }  or q in {(x "/\" y),(x "/\" z)} )
assume  q in  {  (a "/\" b) where a, b is Element of L : ( a in {x} & b in {y,z} )  }  ; ::_thesis: q in {(x "/\" y),(x "/\" z)}
then consider u, v being Element of L such that
A1: q = u "/\" v and
A2: u in {x} and
A3: v in {y,z} ;
A4: ( v = y or v = z ) by A3, TARSKI:def_2;
 u = x by A2, TARSKI:def_1;
hence  q in {(x "/\" y),(x "/\" z)} by A1, A4, TARSKI:def_2; ::_thesis: verum
end;
let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in {(x "/\" y),(x "/\" z)} or q in  {  (a "/\" b) where a, b is Element of L : ( a in {x} & b in {y,z} )  }  )
A5: z in {y,z} by TARSKI:def_2;
assume  q in {(x "/\" y),(x "/\" z)} ; ::_thesis: q in  {  (a "/\" b) where a, b is Element of L : ( a in {x} & b in {y,z} )  }
then A6: ( q = x "/\" y or q = x "/\" z ) by TARSKI:def_2;
 ( x in {x} & y in {y,z} ) by TARSKI:def_1, TARSKI:def_2;
hence  q in  {  (a "/\" b) where a, b is Element of L : ( a in {x} & b in {y,z} )  }  by A6, A5; ::_thesis: verum
end;
end;

theorem :: YELLOW_4:46
for L being non empty RelStr
for x, y being Element of L holds {x} "/\" {y} = {(x "/\" y)} by Lm3;

theorem :: YELLOW_4:47
for L being non empty RelStr
for x, y, z being Element of L holds {x} "/\" {y,z} = {(x "/\" y),(x "/\" z)} by Lm4;

theorem :: YELLOW_4:48
for L being non empty RelStr
for X1, X2, Y1, Y2 being Subset of L st X1 c= Y1 & X2 c= Y2 holds
X1 "/\" X2 c= Y1 "/\" Y2
proof
let L be non empty RelStr ; ::_thesis: for X1, X2, Y1, Y2 being Subset of L st X1 c= Y1 & X2 c= Y2 holds
X1 "/\" X2 c= Y1 "/\" Y2
let X1, X2, Y1, Y2 be Subset of L; ::_thesis: ( X1 c= Y1 & X2 c= Y2 implies X1 "/\" X2 c= Y1 "/\" Y2 )
assume A1: ( X1 c= Y1 & X2 c= Y2 ) ; ::_thesis: X1 "/\" X2 c= Y1 "/\" Y2
let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in X1 "/\" X2 or q in Y1 "/\" Y2 )
assume  q in X1 "/\" X2 ; ::_thesis: q in Y1 "/\" Y2
then  ex x, y being Element of L st
( q = x "/\" y & x in X1 & y in X2 ) ;
hence  q in Y1 "/\" Y2 by A1; ::_thesis: verum
end;

theorem Th49: :: YELLOW_4:49
for L being reflexive antisymmetric with_infima RelStr
for A, B being Subset of L holds A /\ B c= A "/\" B
proof
let L be reflexive antisymmetric with_infima RelStr ; ::_thesis: for A, B being Subset of L holds A /\ B c= A "/\" B
let A, B be Subset of L; ::_thesis: A /\ B c= A "/\" B
let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in A /\ B or q in A "/\" B )
assume A1: q in A /\ B ; ::_thesis: q in A "/\" B
then reconsider A1 = A as non empty Subset of L ;
reconsider q1 = q as Element of A1 by A1, XBOOLE_0:def_4;
A2: q1 = q1 "/\" q1 by YELLOW_0:25;
 q in B by A1, XBOOLE_0:def_4;
hence  q in A "/\" B by A2; ::_thesis: verum
end;

theorem Th50: :: YELLOW_4:50
for L being reflexive antisymmetric with_infima RelStr
for A, B being lower Subset of L holds A "/\" B = A /\ B
proof
let L be reflexive antisymmetric with_infima RelStr ; ::_thesis: for A, B being lower Subset of L holds A "/\" B = A /\ B
let A, B be lower Subset of L; ::_thesis: A "/\" B = A /\ B
thus  A "/\" B c= A /\ B :: according to XBOOLE_0:def_10 ::_thesis: A /\ B c= A "/\" B
proof
let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in A "/\" B or q in A /\ B )
assume  q in A "/\" B ; ::_thesis: q in A /\ B
then consider x, y being Element of L such that
A1: q = x "/\" y and
A2: x in A and
A3: y in B ;
A4: ex z being Element of L st
( x >= z & y >= z & ( for c being Element of L st x >= c & y >= c holds
z >= c ) ) by LATTICE3:def_11;
then  x "/\" y <= y by LATTICE3:def_14;
then A5: q in B by A1, A3, WAYBEL_0:def_19;
 x "/\" y <= x by A4, LATTICE3:def_14;
then  q in A by A1, A2, WAYBEL_0:def_19;
hence  q in A /\ B by A5, XBOOLE_0:def_4; ::_thesis: verum
end;
thus  A /\ B c= A "/\" B by Th49; ::_thesis: verum
end;

theorem :: YELLOW_4:51
for L being reflexive antisymmetric with_infima RelStr
for D being Subset of L
for x being Element of L st x is_>=_than D holds
{x} "/\" D = D
proof
let L be reflexive antisymmetric with_infima RelStr ; ::_thesis: for D being Subset of L
for x being Element of L st x is_>=_than D holds
{x} "/\" D = D
let D be Subset of L; ::_thesis: for x being Element of L st x is_>=_than D holds
{x} "/\" D = D
let x be Element of L; ::_thesis: ( x is_>=_than D implies {x} "/\" D = D )
assume A1: x is_>=_than D ; ::_thesis: {x} "/\" D = D
A2: {x} "/\" D =  {  (x "/\" y) where y is Element of L : y in D  }  by Th42;
thus  {x} "/\" D c= D :: according to XBOOLE_0:def_10 ::_thesis: D c= {x} "/\" D
proof
let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in {x} "/\" D or q in D )
assume  q in {x} "/\" D ; ::_thesis: q in D
then consider y being Element of L such that
A3: q = x "/\" y and
A4: y in D by A2;
 x >= y by A1, A4, LATTICE3:def_9;
hence  q in D by A3, A4, YELLOW_0:25; ::_thesis: verum
end;
let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in D or q in {x} "/\" D )
assume A5: q in D ; ::_thesis: q in {x} "/\" D
then reconsider D1 = D as non empty Subset of L ;
reconsider y = q as Element of D1 by A5;
 x >= y by A1, LATTICE3:def_9;
then  q = x "/\" y by YELLOW_0:25;
hence  q in {x} "/\" D by A2; ::_thesis: verum
end;

theorem :: YELLOW_4:52
for L being antisymmetric with_infima RelStr
for D being Subset of L
for x being Element of L holds {x} "/\" D is_<=_than x
proof
let L be antisymmetric with_infima RelStr ; ::_thesis: for D being Subset of L
for x being Element of L holds {x} "/\" D is_<=_than x
let D be Subset of L; ::_thesis: for x being Element of L holds {x} "/\" D is_<=_than x
let x be Element of L; ::_thesis: {x} "/\" D is_<=_than x
let b be Element of L; :: according to LATTICE3:def_9 ::_thesis: ( not b in {x} "/\" D or b <= x )
A1: {x} "/\" D =  {  (x "/\" h) where h is Element of L : h in D  }  by Th42;
assume  b in {x} "/\" D ; ::_thesis: b <= x
then consider h being Element of L such that
A2: b = x "/\" h and
 h in D by A1;
 ex w being Element of L st
( x >= w & h >= w & ( for c being Element of L st x >= c & h >= c holds
w >= c ) ) by LATTICE3:def_11;
hence  b <= x by A2, LATTICE3:def_14; ::_thesis: verum
end;

theorem :: YELLOW_4:53
for L being Semilattice
for X being Subset of L
for x being Element of L st ex_sup_of {x} "/\" X,L & ex_sup_of X,L holds
sup ({x} "/\" X) <= x "/\" (sup X)
proof
let L be Semilattice; ::_thesis: for X being Subset of L
for x being Element of L st ex_sup_of {x} "/\" X,L & ex_sup_of X,L holds
sup ({x} "/\" X) <= x "/\" (sup X)
let X be Subset of L; ::_thesis: for x being Element of L st ex_sup_of {x} "/\" X,L & ex_sup_of X,L holds
sup ({x} "/\" X) <= x "/\" (sup X)
let x be Element of L; ::_thesis: ( ex_sup_of {x} "/\" X,L & ex_sup_of X,L implies sup ({x} "/\" X) <= x "/\" (sup X) )
assume that
A1: ex_sup_of {x} "/\" X,L and
A2: ex_sup_of X,L ; ::_thesis: sup ({x} "/\" X) <= x "/\" (sup X)
A3: {x} "/\" X =  {  (x "/\" y) where y is Element of L : y in X  }  by Th42;
 {x} "/\" X is_<=_than x "/\" (sup X)
proof
let q be Element of L; :: according to LATTICE3:def_9 ::_thesis: ( not q in {x} "/\" X or q <= x "/\" (sup X) )
assume  q in {x} "/\" X ; ::_thesis: q <= x "/\" (sup X)
then consider y being Element of L such that
A4: q = x "/\" y and
A5: y in X by A3;
 ( x <= x & y <= sup X ) by A2, A5, Th1;
hence  q <= x "/\" (sup X) by A4, YELLOW_3:2; ::_thesis: verum
end;
hence  sup ({x} "/\" X) <= x "/\" (sup X) by A1, YELLOW_0:def_9; ::_thesis: verum
end;

theorem Th54: :: YELLOW_4:54
for L being non empty transitive antisymmetric complete RelStr
for A being Subset of L
for B being non empty Subset of L holds A is_>=_than inf (A "/\" B)
proof
let L be non empty transitive antisymmetric complete RelStr ; ::_thesis: for A being Subset of L
for B being non empty Subset of L holds A is_>=_than inf (A "/\" B)
let A be Subset of L; ::_thesis: for B being non empty Subset of L holds A is_>=_than inf (A "/\" B)
let B be non empty Subset of L; ::_thesis: A is_>=_than inf (A "/\" B)
set b = the Element of B;
let x be Element of L; :: according to LATTICE3:def_8 ::_thesis: ( not x in A or inf (A "/\" B) <= x )
assume  x in A ; ::_thesis: inf (A "/\" B) <= x
then A1: x "/\" the Element of B in A "/\" B ;
 ex xx being Element of L st
( x >= xx & the Element of B >= xx & ( for c being Element of L st x >= c & the Element of B >= c holds
xx >= c ) ) by LATTICE3:def_11;
then A2: x >= x "/\" the Element of B by LATTICE3:def_14;
 ex_inf_of A "/\" B,L by YELLOW_0:17;
then  A "/\" B is_>=_than inf (A "/\" B) by YELLOW_0:def_10;
then  x "/\" the Element of B >= inf (A "/\" B) by A1, LATTICE3:def_8;
hence  inf (A "/\" B) <= x by A2, YELLOW_0:def_2; ::_thesis: verum
end;

theorem Th55: :: YELLOW_4:55
for L being transitive antisymmetric with_infima RelStr
for a, b being Element of L
for A, B being Subset of L st a is_<=_than A & b is_<=_than B holds
a "/\" b is_<=_than A "/\" B
proof
let L be transitive antisymmetric with_infima RelStr ; ::_thesis: for a, b being Element of L
for A, B being Subset of L st a is_<=_than A & b is_<=_than B holds
a "/\" b is_<=_than A "/\" B
let a, b be Element of L; ::_thesis: for A, B being Subset of L st a is_<=_than A & b is_<=_than B holds
a "/\" b is_<=_than A "/\" B
let A, B be Subset of L; ::_thesis: ( a is_<=_than A & b is_<=_than B implies a "/\" b is_<=_than A "/\" B )
assume A1: ( a is_<=_than A & b is_<=_than B ) ; ::_thesis: a "/\" b is_<=_than A "/\" B
let q be Element of L; :: according to LATTICE3:def_8 ::_thesis: ( not q in A "/\" B or a "/\" b <= q )
assume  q in A "/\" B ; ::_thesis: a "/\" b <= q
then consider x, y being Element of L such that
A2: q = x "/\" y and
A3: ( x in A & y in B ) ;
 ( a <= x & b <= y ) by A1, A3, LATTICE3:def_8;
hence  a "/\" b <= q by A2, YELLOW_3:2; ::_thesis: verum
end;

theorem :: YELLOW_4:56
for L being transitive antisymmetric with_infima RelStr
for a, b being Element of L
for A, B being Subset of L st a is_>=_than A & b is_>=_than B holds
a "/\" b is_>=_than A "/\" B
proof
let L be transitive antisymmetric with_infima RelStr ; ::_thesis: for a, b being Element of L
for A, B being Subset of L st a is_>=_than A & b is_>=_than B holds
a "/\" b is_>=_than A "/\" B
let a, b be Element of L; ::_thesis: for A, B being Subset of L st a is_>=_than A & b is_>=_than B holds
a "/\" b is_>=_than A "/\" B
let A, B be Subset of L; ::_thesis: ( a is_>=_than A & b is_>=_than B implies a "/\" b is_>=_than A "/\" B )
assume A1: ( a is_>=_than A & b is_>=_than B ) ; ::_thesis: a "/\" b is_>=_than A "/\" B
let q be Element of L; :: according to LATTICE3:def_9 ::_thesis: ( not q in A "/\" B or q <= a "/\" b )
assume  q in A "/\" B ; ::_thesis: q <= a "/\" b
then consider x, y being Element of L such that
A2: q = x "/\" y and
A3: ( x in A & y in B ) ;
 ( a >= x & b >= y ) by A1, A3, LATTICE3:def_9;
hence  q <= a "/\" b by A2, YELLOW_3:2; ::_thesis: verum
end;

theorem :: YELLOW_4:57
for L being non empty complete Poset
for A, B being non empty Subset of L holds inf (A "/\" B) = (inf A) "/\" (inf B)
proof
let L be non empty complete Poset; ::_thesis: for A, B being non empty Subset of L holds inf (A "/\" B) = (inf A) "/\" (inf B)
let A, B be non empty Subset of L; ::_thesis: inf (A "/\" B) = (inf A) "/\" (inf B)
 B is_>=_than inf (A "/\" B) by Th54;
then A1: inf B >= inf (A "/\" B) by YELLOW_0:33;
 A is_>=_than inf (A "/\" B) by Th54;
then  inf A >= inf (A "/\" B) by YELLOW_0:33;
then A2: (inf A) "/\" (inf B) >= (inf (A "/\" B)) "/\" (inf (A "/\" B)) by A1, YELLOW_3:2;
 ( A is_>=_than inf A & B is_>=_than inf B ) by YELLOW_0:33;
then  ( ex_inf_of A "/\" B,L & A "/\" B is_>=_than (inf A) "/\" (inf B) ) by Th55, YELLOW_0:17;
then A3: inf (A "/\" B) >= (inf A) "/\" (inf B) by YELLOW_0:def_10;
 (inf (A "/\" B)) "/\" (inf (A "/\" B)) = inf (A "/\" B) by YELLOW_0:25;
hence  inf (A "/\" B) = (inf A) "/\" (inf B) by A3, A2, ORDERS_2:2; ::_thesis: verum
end;

theorem :: YELLOW_4:58
for L being Semilattice
for x, y being Element of (InclPoset (Ids L))
for x1, y1 being Subset of L st x = x1 & y = y1 holds
x "/\" y = x1 "/\" y1
proof
let L be Semilattice; ::_thesis: for x, y being Element of (InclPoset (Ids L))
for x1, y1 being Subset of L st x = x1 & y = y1 holds
x "/\" y = x1 "/\" y1
let x, y be Element of (InclPoset (Ids L)); ::_thesis: for x1, y1 being Subset of L st x = x1 & y = y1 holds
x "/\" y = x1 "/\" y1
let x1, y1 be Subset of L; ::_thesis: ( x = x1 & y = y1 implies x "/\" y = x1 "/\" y1 )
assume A1: ( x = x1 & y = y1 ) ; ::_thesis: x "/\" y = x1 "/\" y1
then A2: ( x1 is lower & y1 is lower ) by YELLOW_2:41;
thus x "/\" y = x /\ y by YELLOW_2:43
.= x1 "/\" y1 by A1, A2, Th50 ; ::_thesis: verum
end;

theorem :: YELLOW_4:59
for L being antisymmetric with_infima RelStr
for X being Subset of L
for Y being non empty Subset of L holds X c= uparrow (X "/\" Y)
proof
let L be antisymmetric with_infima RelStr ; ::_thesis: for X being Subset of L
for Y being non empty Subset of L holds X c= uparrow (X "/\" Y)
let X be Subset of L; ::_thesis: for Y being non empty Subset of L holds X c= uparrow (X "/\" Y)
let Y be non empty Subset of L; ::_thesis: X c= uparrow (X "/\" Y)
consider y being set  such that
A1: y in Y by XBOOLE_0:def_1;
reconsider y = y as Element of Y by A1;
let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in X or q in uparrow (X "/\" Y) )
assume A2: q in X ; ::_thesis: q in uparrow (X "/\" Y)
then reconsider X1 = X as non empty Subset of L ;
reconsider x = q as Element of X1 by A2;
 ex s being Element of L st
( x >= s & y >= s & ( for c being Element of L st x >= c & y >= c holds
s >= c ) ) by LATTICE3:def_11;
then A3: x "/\" y <= x by LATTICE3:def_14;
 ( uparrow (X "/\" Y) =  {  s where s is Element of L : ex y being Element of L st
( s >= y & y in X "/\" Y )  }  & x "/\" y in X1 "/\" Y ) by WAYBEL_0:15;
hence  q in uparrow (X "/\" Y) by A3; ::_thesis: verum
end;

theorem :: YELLOW_4:60
for L being non empty RelStr
for D being Subset of [:L,L:] holds union  {  X where X is Subset of L : ex x being Element of L st
( X = {x} "/\" (proj2 D) & x in proj1 D )  }  = (proj1 D) "/\" (proj2 D)
proof
let L be non empty RelStr ; ::_thesis: for D being Subset of [:L,L:] holds union  {  X where X is Subset of L : ex x being Element of L st
( X = {x} "/\" (proj2 D) & x in proj1 D )  }  = (proj1 D) "/\" (proj2 D)
let D be Subset of [:L,L:]; ::_thesis: union  {  X where X is Subset of L : ex x being Element of L st
( X = {x} "/\" (proj2 D) & x in proj1 D )  }  = (proj1 D) "/\" (proj2 D)
set D1 = proj1 D;
set D2 = proj2 D;
defpred S1[ set ] means  ex x being Element of L st
( $1 = {x} "/\" (proj2 D) & x in proj1 D );
thus  union  {  X where X is Subset of L : S1[X]  }  c= (proj1 D) "/\" (proj2 D) :: according to XBOOLE_0:def_10 ::_thesis: (proj1 D) "/\" (proj2 D) c= union  {  X where X is Subset of L : ex x being Element of L st
( X = {x} "/\" (proj2 D) & x in proj1 D )  }
proof
let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in union  {  X where X is Subset of L : S1[X]  }  or q in (proj1 D) "/\" (proj2 D) )
assume  q in union  {  X where X is Subset of L : S1[X]  }  ; ::_thesis: q in (proj1 D) "/\" (proj2 D)
then consider w being set  such that
A1: q in w and
A2: w in  {  X where X is Subset of L : S1[X]  }  by TARSKI:def_4;
consider e being Subset of L such that
A3: w = e and
A4: S1[e] by A2;
consider p being Element of L such that
A5: e = {p} "/\" (proj2 D) and
A6: p in proj1 D by A4;
 {p} "/\" (proj2 D) =  {  (p "/\" y) where y is Element of L : y in proj2 D  }  by Th42;
then  ex y being Element of L st
( q = p "/\" y & y in proj2 D ) by A1, A3, A5;
hence  q in (proj1 D) "/\" (proj2 D) by A6; ::_thesis: verum
end;
let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in (proj1 D) "/\" (proj2 D) or q in union  {  X where X is Subset of L : ex x being Element of L st
( X = {x} "/\" (proj2 D) & x in proj1 D )  }  )
assume  q in (proj1 D) "/\" (proj2 D) ; ::_thesis: q in union  {  X where X is Subset of L : ex x being Element of L st
( X = {x} "/\" (proj2 D) & x in proj1 D )  }
then consider x, y being Element of L such that
A7: q = x "/\" y and
A8: x in proj1 D and
A9: y in proj2 D ;
 {x} "/\" (proj2 D) =  {  (x "/\" d) where d is Element of L : d in proj2 D  }  by Th42;
then A10: q in {x} "/\" (proj2 D) by A7, A9;
 {x} "/\" (proj2 D) in  {  X where X is Subset of L : S1[X]  }  by A8;
hence  q in union  {  X where X is Subset of L : ex x being Element of L st
( X = {x} "/\" (proj2 D) & x in proj1 D )  }  by A10, TARSKI:def_4; ::_thesis: verum
end;

theorem Th61: :: YELLOW_4:61
for L being transitive antisymmetric with_infima RelStr
for D1, D2 being Subset of L holds downarrow ((downarrow D1) "/\" (downarrow D2)) c= downarrow (D1 "/\" D2)
proof
let L be transitive antisymmetric with_infima RelStr ; ::_thesis: for D1, D2 being Subset of L holds downarrow ((downarrow D1) "/\" (downarrow D2)) c= downarrow (D1 "/\" D2)
let D1, D2 be Subset of L; ::_thesis: downarrow ((downarrow D1) "/\" (downarrow D2)) c= downarrow (D1 "/\" D2)
A1: downarrow ((downarrow D1) "/\" (downarrow D2)) =  {  x where x is Element of L : ex t being Element of L st
( x <= t & t in (downarrow D1) "/\" (downarrow D2) )  }  by WAYBEL_0:14;
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in downarrow ((downarrow D1) "/\" (downarrow D2)) or y in downarrow (D1 "/\" D2) )
assume  y in downarrow ((downarrow D1) "/\" (downarrow D2)) ; ::_thesis: y in downarrow (D1 "/\" D2)
then consider x being Element of L such that
A2: y = x and
A3: ex t being Element of L st
( x <= t & t in (downarrow D1) "/\" (downarrow D2) ) by A1;
consider x1 being Element of L such that
A4: x <= x1 and
A5: x1 in (downarrow D1) "/\" (downarrow D2) by A3;
consider a, b being Element of L such that
A6: x1 = a "/\" b and
A7: a in downarrow D1 and
A8: b in downarrow D2 by A5;
 downarrow D2 =  {  s2 where s2 is Element of L : ex z being Element of L st
( s2 <= z & z in D2 )  }  by WAYBEL_0:14;
then consider B1 being Element of L such that
A9: b = B1 and
A10: ex z being Element of L st
( B1 <= z & z in D2 ) by A8;
consider b1 being Element of L such that
A11: B1 <= b1 and
A12: b1 in D2 by A10;
 downarrow D1 =  {  s1 where s1 is Element of L : ex z being Element of L st
( s1 <= z & z in D1 )  }  by WAYBEL_0:14;
then consider A1 being Element of L such that
A13: a = A1 and
A14: ex z being Element of L st
( A1 <= z & z in D1 ) by A7;
consider a1 being Element of L such that
A15: A1 <= a1 and
A16: a1 in D1 by A14;
 x1 <= a1 "/\" b1 by A6, A13, A9, A15, A11, YELLOW_3:2;
then A17: ( downarrow (D1 "/\" D2) =  {  s where s is Element of L : ex z being Element of L st
( s <= z & z in D1 "/\" D2 )  }  & x <= a1 "/\" b1 ) by A4, ORDERS_2:3, WAYBEL_0:14;
 a1 "/\" b1 in D1 "/\" D2 by A16, A12;
hence  y in downarrow (D1 "/\" D2) by A2, A17; ::_thesis: verum
end;

theorem :: YELLOW_4:62
for L being Semilattice
for D1, D2 being Subset of L holds downarrow ((downarrow D1) "/\" (downarrow D2)) = downarrow (D1 "/\" D2)
proof
let L be Semilattice; ::_thesis: for D1, D2 being Subset of L holds downarrow ((downarrow D1) "/\" (downarrow D2)) = downarrow (D1 "/\" D2)
let D1, D2 be Subset of L; ::_thesis: downarrow ((downarrow D1) "/\" (downarrow D2)) = downarrow (D1 "/\" D2)
A1: downarrow (D1 "/\" D2) =  {  s where s is Element of L : ex z being Element of L st
( s <= z & z in D1 "/\" D2 )  }  by WAYBEL_0:14;
thus  downarrow ((downarrow D1) "/\" (downarrow D2)) c= downarrow (D1 "/\" D2) by Th61; :: according to XBOOLE_0:def_10 ::_thesis: downarrow (D1 "/\" D2) c= downarrow ((downarrow D1) "/\" (downarrow D2))
let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in downarrow (D1 "/\" D2) or q in downarrow ((downarrow D1) "/\" (downarrow D2)) )
assume  q in downarrow (D1 "/\" D2) ; ::_thesis: q in downarrow ((downarrow D1) "/\" (downarrow D2))
then consider s being Element of L such that
A2: q = s and
A3: ex z being Element of L st
( s <= z & z in D1 "/\" D2 ) by A1;
A4: downarrow ((downarrow D1) "/\" (downarrow D2)) =  {  x where x is Element of L : ex t being Element of L st
( x <= t & t in (downarrow D1) "/\" (downarrow D2) )  }  by WAYBEL_0:14;
A5: ( D1 is Subset of (downarrow D1) & D2 is Subset of (downarrow D2) ) by WAYBEL_0:16;
consider x being Element of L such that
A6: s <= x and
A7: x in D1 "/\" D2 by A3;
 ex a, b being Element of L st
( x = a "/\" b & a in D1 & b in D2 ) by A7;
then  x in (downarrow D1) "/\" (downarrow D2) by A5;
hence  q in downarrow ((downarrow D1) "/\" (downarrow D2)) by A4, A2, A6; ::_thesis: verum
end;

theorem Th63: :: YELLOW_4:63
for L being transitive antisymmetric with_infima RelStr
for D1, D2 being Subset of L holds uparrow ((uparrow D1) "/\" (uparrow D2)) c= uparrow (D1 "/\" D2)
proof
let L be transitive antisymmetric with_infima RelStr ; ::_thesis: for D1, D2 being Subset of L holds uparrow ((uparrow D1) "/\" (uparrow D2)) c= uparrow (D1 "/\" D2)
let D1, D2 be Subset of L; ::_thesis: uparrow ((uparrow D1) "/\" (uparrow D2)) c= uparrow (D1 "/\" D2)
A1: uparrow ((uparrow D1) "/\" (uparrow D2)) =  {  x where x is Element of L : ex t being Element of L st
( x >= t & t in (uparrow D1) "/\" (uparrow D2) )  }  by WAYBEL_0:15;
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in uparrow ((uparrow D1) "/\" (uparrow D2)) or y in uparrow (D1 "/\" D2) )
assume  y in uparrow ((uparrow D1) "/\" (uparrow D2)) ; ::_thesis: y in uparrow (D1 "/\" D2)
then consider x being Element of L such that
A2: y = x and
A3: ex t being Element of L st
( x >= t & t in (uparrow D1) "/\" (uparrow D2) ) by A1;
consider x1 being Element of L such that
A4: x >= x1 and
A5: x1 in (uparrow D1) "/\" (uparrow D2) by A3;
consider a, b being Element of L such that
A6: x1 = a "/\" b and
A7: a in uparrow D1 and
A8: b in uparrow D2 by A5;
 uparrow D2 =  {  s2 where s2 is Element of L : ex z being Element of L st
( s2 >= z & z in D2 )  }  by WAYBEL_0:15;
then consider B1 being Element of L such that
A9: b = B1 and
A10: ex z being Element of L st
( B1 >= z & z in D2 ) by A8;
consider b1 being Element of L such that
A11: B1 >= b1 and
A12: b1 in D2 by A10;
 uparrow D1 =  {  s1 where s1 is Element of L : ex z being Element of L st
( s1 >= z & z in D1 )  }  by WAYBEL_0:15;
then consider A1 being Element of L such that
A13: a = A1 and
A14: ex z being Element of L st
( A1 >= z & z in D1 ) by A7;
consider a1 being Element of L such that
A15: A1 >= a1 and
A16: a1 in D1 by A14;
 x1 >= a1 "/\" b1 by A6, A13, A9, A15, A11, YELLOW_3:2;
then A17: ( uparrow (D1 "/\" D2) =  {  s where s is Element of L : ex z being Element of L st
( s >= z & z in D1 "/\" D2 )  }  & x >= a1 "/\" b1 ) by A4, ORDERS_2:3, WAYBEL_0:15;
 a1 "/\" b1 in D1 "/\" D2 by A16, A12;
hence  y in uparrow (D1 "/\" D2) by A2, A17; ::_thesis: verum
end;

theorem :: YELLOW_4:64
for L being Semilattice
for D1, D2 being Subset of L holds uparrow ((uparrow D1) "/\" (uparrow D2)) = uparrow (D1 "/\" D2)
proof
let L be Semilattice; ::_thesis: for D1, D2 being Subset of L holds uparrow ((uparrow D1) "/\" (uparrow D2)) = uparrow (D1 "/\" D2)
let D1, D2 be Subset of L; ::_thesis: uparrow ((uparrow D1) "/\" (uparrow D2)) = uparrow (D1 "/\" D2)
A1: uparrow (D1 "/\" D2) =  {  s where s is Element of L : ex z being Element of L st
( s >= z & z in D1 "/\" D2 )  }  by WAYBEL_0:15;
thus  uparrow ((uparrow D1) "/\" (uparrow D2)) c= uparrow (D1 "/\" D2) by Th63; :: according to XBOOLE_0:def_10 ::_thesis: uparrow (D1 "/\" D2) c= uparrow ((uparrow D1) "/\" (uparrow D2))
let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in uparrow (D1 "/\" D2) or q in uparrow ((uparrow D1) "/\" (uparrow D2)) )
assume  q in uparrow (D1 "/\" D2) ; ::_thesis: q in uparrow ((uparrow D1) "/\" (uparrow D2))
then consider s being Element of L such that
A2: q = s and
A3: ex z being Element of L st
( s >= z & z in D1 "/\" D2 ) by A1;
A4: uparrow ((uparrow D1) "/\" (uparrow D2)) =  {  x where x is Element of L : ex t being Element of L st
( x >= t & t in (uparrow D1) "/\" (uparrow D2) )  }  by WAYBEL_0:15;
A5: ( D1 is Subset of (uparrow D1) & D2 is Subset of (uparrow D2) ) by WAYBEL_0:16;
consider x being Element of L such that
A6: s >= x and
A7: x in D1 "/\" D2 by A3;
 ex a, b being Element of L st
( x = a "/\" b & a in D1 & b in D2 ) by A7;
then  x in (uparrow D1) "/\" (uparrow D2) by A5;
hence  q in uparrow ((uparrow D1) "/\" (uparrow D2)) by A4, A2, A6; ::_thesis: verum
end;