let L be Semilattice; :: thesis: for D being non empty directed Subset of [:L,L:] holds union { X where X is non empty directed 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 non empty directed Subset of [:L,L:]; :: thesis: union { X where X is non empty directed 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 S₁[ set ] means ex x being Element of L st
( $1 = {x} "/\" (proj2 D) & x in proj1 D );
reconsider T = proj2 D as non empty directed Subset of L by YELLOW_3:21, YELLOW_3:22;
A1: (proj1 D) "/\" (proj2 D) = { (x "/\" y) where x, y is Element of L : ( x in proj1 D & y in proj2 D ) } by YELLOW_4:def 4;
thus union { X where X is non empty directed Subset of L : S₁[X] } c= (proj1 D) "/\" (proj2 D) :: according to XBOOLE_0:def 10 :: thesis: (proj1 D) "/\" (proj2 D) c= union { X where X is non empty directed Subset of L : ex x being Element of L st
( X = {x} "/\" (proj2 D) & x in proj1 D ) }

proof

let q be object ; :: according to TARSKI:def 3 :: thesis: ( not q in union { X where X is non empty directed Subset of L : S₁[X] } or q in (proj1 D) "/\" (proj2 D) )
assume q in union { X where X is non empty directed Subset of L : S₁[X] } ; :: thesis: q in (proj1 D) "/\" (proj2 D)
then consider w being set such that
A2: q in w and
A3: w in { X where X is non empty directed Subset of L : S₁[X] } by TARSKI:def 4;
consider e being non empty directed Subset of L such that
A4: w = e and
A5: S₁[e] by A3;
consider p being Element of L such that
A6: e = {p} "/\" (proj2 D) and
A7: p in proj1 D by A5;
{p} "/\" (proj2 D) = { (p "/\" y) where y is Element of L : y in proj2 D } by YELLOW_4:42;
then ex y being Element of L st
( q = p "/\" y & y in proj2 D ) by A2, A4, A6;
hence q in (proj1 D) "/\" (proj2 D) by A1, A7; :: thesis: verum

end;

let q be object ; :: according to TARSKI:def 3 :: thesis: ( not q in (proj1 D) "/\" (proj2 D) or q in union { X where X is non empty directed 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 non empty directed 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
A8: q = x "/\" y and
A9: x in proj1 D and
A10: y in proj2 D by A1;
reconsider xx = {x} as non empty directed Subset of L by WAYBEL_0:5;
( not xx "/\" T is empty & xx "/\" T is directed ) ;
then A11: {x} "/\" (proj2 D) in { X where X is non empty directed Subset of L : S₁[X] } by A9;
{x} "/\" (proj2 D) = { (x "/\" d) where d is Element of L : d in proj2 D } by YELLOW_4:42;
then q in {x} "/\" (proj2 D) by A8, A10;
hence q in union { X where X is non empty directed Subset of L : ex x being Element of L st
( X = {x} "/\" (proj2 D) & x in proj1 D ) } by A11, TARSKI:def 4; :: thesis: verum