:: Definitions and Properties of the Join and Meet of Subsets
:: by Artur Korni{\l}owicz
::
:: Received September 25, 1996
:: Copyright (c) 1996-2012 Association of Mizar Users


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)
proofend;

theorem Th2: :: YELLOW_4:2
for L being RelStr
for X being set
for a being Element of L st a in X &amp; ex_inf_of X,L holds
"/\" (X,L) <= a
proofend;

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 &amp; 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 &amp; 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 &amp; 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 &amp; 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)
proofend;
:: original:is_coarser_than
redefine predB is_coarser_than A;
reflexivity
 for B being Subset of L holds (L,b1,b1)
proofend;
end;

theorem :: YELLOW_4:3
for L being RelStr
for B being Subset of L holds {} L is_finer_than B
proofend;

theorem :: YELLOW_4:4
for L being transitive RelStr
for A, B, C being Subset of L st A is_finer_than B &amp; B is_finer_than C holds
A is_finer_than C
proofend;

theorem :: YELLOW_4:5
for L being RelStr
for A, B being Subset of L st B is_finer_than A &amp; A is lower holds
B c= A
proofend;

theorem :: YELLOW_4:6
for L being RelStr
for A being Subset of L holds {} L is_coarser_than A
proofend;

theorem :: YELLOW_4:7
for L being transitive RelStr
for A, B, C being Subset of L st C is_coarser_than B &amp; B is_coarser_than A holds
C is_coarser_than A
proofend;

theorem :: YELLOW_4:8
for L being RelStr
for A, B being Subset of L st A is_coarser_than B &amp; B is upper holds
A c= B
proofend;

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 &amp; y in D2 )  }  ;
coherence
  {  (x "\/" y) where x, y is Element of L : ( x in D1 &amp; y in D2 )  }  is Subset of L
proofend;
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 &amp; 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
proofend;
end;

theorem :: YELLOW_4:9
for L being non empty RelStr
for X being Subset of L holds X "\/" ({} L) = {}
proofend;

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 &amp; 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
proofend;

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

theorem :: YELLOW_4:13
for L being reflexive antisymmetric with_suprema RelStr
for A being Subset of L holds A c= A "\/" A
proofend;

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)
proofend;

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
proofend;
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
proofend;
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
proofend;
end;

registration
let L be with_suprema Poset;
let D1, D2 be upper Subset of L;
clusterD1 "\/" D2 ->  upper ;
coherence
 D1 "\/" D2 is upper
proofend;
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  }
proofend;

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)
proofend;

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)
proofend;

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)
proofend;

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}_&amp;_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} &amp; 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} &amp; b in {y} )  }  = {(x "\/" y)}
thus   {  (a "\/" b) where a, b is Element of L : ( a in {x} &amp; b in {y} )  }  = {(x "\/" y)} ::_thesis: verum
proof
thus   {  (a "\/" b) where a, b is Element of L : ( a in {x} &amp; b in {y} )  }  c= {(x "\/" y)} :: according toXBOOLE_0:def_10 ::_thesis: {(x "\/" y)} c=  {  (a "\/" b) where a, b is Element of L : ( a in {x} &amp; b in {y} )  }
proof
let q be set ; :: according toTARSKI:def_3 ::_thesis: ( not q in  {  (a "\/" b) where a, b is Element of L : ( a in {x} &amp; b in {y} )  }  or q in {(x "\/" y)} )
assume  q in  {  (a "\/" b) where a, b is Element of L : ( a in {x} &amp; 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} &amp; v in {y} ) ;
 ( u = x &amp; 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 toTARSKI:def_3 ::_thesis: ( not q in {(x "\/" y)} or q in  {  (a "\/" b) where a, b is Element of L : ( a in {x} &amp; b in {y} )  }  )
assume  q in {(x "\/" y)} ; ::_thesis: q in  {  (a "\/" b) where a, b is Element of L : ( a in {x} &amp; b in {y} )  }
then A3: q = x "\/" y by TARSKI:def_1;
 ( x in {x} &amp; y in {y} ) by TARSKI:def_1;
hence  q in  {  (a "\/" b) where a, b is Element of L : ( a in {x} &amp; 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}_&amp;_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} &amp; 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} &amp; b in {y,z} )  }  = {(x "\/" y),(x "\/" z)}
thus   {  (a "\/" b) where a, b is Element of L : ( a in {x} &amp; b in {y,z} )  }  = {(x "\/" y),(x "\/" z)} ::_thesis: verum
proof
thus   {  (a "\/" b) where a, b is Element of L : ( a in {x} &amp; b in {y,z} )  }  c= {(x "\/" y),(x "\/" z)} :: according toXBOOLE_0:def_10 ::_thesis: {(x "\/" y),(x "\/" z)} c=  {  (a "\/" b) where a, b is Element of L : ( a in {x} &amp; b in {y,z} )  }
proof
let q be set ; :: according toTARSKI:def_3 ::_thesis: ( not q in  {  (a "\/" b) where a, b is Element of L : ( a in {x} &amp; 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} &amp; 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 toTARSKI: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} &amp; 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} &amp; b in {y,z} )  }
then A6: ( q = x "\/" y or q = x "\/" z ) by TARSKI:def_2;
 ( x in {x} &amp; 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} &amp; 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 &amp; X2 c= Y2 holds
X1 "\/" X2 c= Y1 "\/" Y2
proofend;

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

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

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 &amp; ex_inf_of X,L holds
x "\/" (inf X) <= inf ({x} "\/" X)
proofend;

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)
proofend;

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 &amp; b is_<=_than B holds
a "\/" b is_<=_than A "\/" B
proofend;

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 &amp; b is_>=_than B holds
a "\/" b is_>=_than A "\/" B
proofend;

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)
proofend;

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)
proofend;

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 &amp; y = Y holds
x "\/" y = downarrow (X "\/" Y)
proofend;

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) &amp; x in proj1 D )  }  = (proj1 D) "\/" (proj2 D)
proofend;

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)
proofend;

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)
proofend;

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)
proofend;

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)
proofend;

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 &amp; y in D2 )  }  ;
coherence
  {  (x "/\" y) where x, y is Element of L : ( x in D1 &amp; y in D2 )  }  is Subset of L
proofend;
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 &amp; 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
proofend;
end;

theorem :: YELLOW_4:36
for L being non empty RelStr
for X being Subset of L holds X "/\" ({} L) = {}
proofend;

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 &amp; 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
proofend;

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

theorem :: YELLOW_4:40
for L being reflexive antisymmetric with_infima RelStr
for A being Subset of L holds A c= A "/\" A
proofend;

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)
proofend;

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
proofend;
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
proofend;
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
proofend;
end;

registration
let L be Semilattice;
let D1, D2 be lower Subset of L;
clusterD1 "/\" D2 ->  lower ;
coherence
 D1 "/\" D2 is lower
proofend;
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  }
proofend;

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)
proofend;

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)
proofend;

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)
proofend;

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}_&amp;_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} &amp; 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} &amp; b in {y} )  }  = {(x "/\" y)}
thus   {  (a "/\" b) where a, b is Element of L : ( a in {x} &amp; b in {y} )  }  = {(x "/\" y)} ::_thesis: verum
proof
thus   {  (a "/\" b) where a, b is Element of L : ( a in {x} &amp; b in {y} )  }  c= {(x "/\" y)} :: according toXBOOLE_0:def_10 ::_thesis: {(x "/\" y)} c=  {  (a "/\" b) where a, b is Element of L : ( a in {x} &amp; b in {y} )  }
proof
let q be set ; :: according toTARSKI:def_3 ::_thesis: ( not q in  {  (a "/\" b) where a, b is Element of L : ( a in {x} &amp; b in {y} )  }  or q in {(x "/\" y)} )
assume  q in  {  (a "/\" b) where a, b is Element of L : ( a in {x} &amp; 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} &amp; v in {y} ) ;
 ( u = x &amp; 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 toTARSKI:def_3 ::_thesis: ( not q in {(x "/\" y)} or q in  {  (a "/\" b) where a, b is Element of L : ( a in {x} &amp; b in {y} )  }  )
assume  q in {(x "/\" y)} ; ::_thesis: q in  {  (a "/\" b) where a, b is Element of L : ( a in {x} &amp; b in {y} )  }
then A3: q = x "/\" y by TARSKI:def_1;
 ( x in {x} &amp; y in {y} ) by TARSKI:def_1;
hence  q in  {  (a "/\" b) where a, b is Element of L : ( a in {x} &amp; 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}_&amp;_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} &amp; 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} &amp; b in {y,z} )  }  = {(x "/\" y),(x "/\" z)}
thus   {  (a "/\" b) where a, b is Element of L : ( a in {x} &amp; b in {y,z} )  }  = {(x "/\" y),(x "/\" z)} ::_thesis: verum
proof
thus   {  (a "/\" b) where a, b is Element of L : ( a in {x} &amp; b in {y,z} )  }  c= {(x "/\" y),(x "/\" z)} :: according toXBOOLE_0:def_10 ::_thesis: {(x "/\" y),(x "/\" z)} c=  {  (a "/\" b) where a, b is Element of L : ( a in {x} &amp; b in {y,z} )  }
proof
let q be set ; :: according toTARSKI:def_3 ::_thesis: ( not q in  {  (a "/\" b) where a, b is Element of L : ( a in {x} &amp; 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} &amp; 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 toTARSKI: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} &amp; 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} &amp; b in {y,z} )  }
then A6: ( q = x "/\" y or q = x "/\" z ) by TARSKI:def_2;
 ( x in {x} &amp; 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} &amp; 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 &amp; X2 c= Y2 holds
X1 "/\" X2 c= Y1 "/\" Y2
proofend;

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

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

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

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

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 &amp; ex_sup_of X,L holds
sup ({x} "/\" X) <= x "/\" (sup X)
proofend;

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)
proofend;

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 &amp; b is_<=_than B holds
a "/\" b is_<=_than A "/\" B
proofend;

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 &amp; b is_>=_than B holds
a "/\" b is_>=_than A "/\" B
proofend;

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)
proofend;

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 &amp; y = y1 holds
x "/\" y = x1 "/\" y1
proofend;

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)
proofend;

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) &amp; x in proj1 D )  }  = (proj1 D) "/\" (proj2 D)
proofend;

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)
proofend;

theorem :: YELLOW_4:62
for L being Semilattice
for D1, D2 being Subset of L holds downarrow ((downarrow D1) "/\" (downarrow D2)) = downarrow (D1 "/\" D2)
proofend;

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)
proofend;

theorem :: YELLOW_4:64
for L being Semilattice
for D1, D2 being Subset of L holds uparrow ((uparrow D1) "/\" (uparrow D2)) = uparrow (D1 "/\" D2)
proofend;