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

set D1 = proj1 D;
set D2 = proj2 D;
defpred S1[ set ] means ex x being Element of L st
( \$1 = {x} "/\" () & x in proj1 D );
reconsider T = proj2 D as non empty directed Subset of L by ;
A1: (proj1 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 : S1[X] } c= () "/\" () :: according to XBOOLE_0:def 10 :: thesis: () "/\" () c= union { X where X is non empty directed Subset of L : ex x being Element of L st
( X = {x} "/\" () & 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 : S1[X] } or q in () "/\" () )
assume q in union { X where X is non empty directed Subset of L : S1[X] } ; :: thesis: q in () "/\" ()
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 : S1[X] } by TARSKI:def 4;
consider e being non empty directed Subset of L such that
A4: w = e and
A5: S1[e] by A3;
consider p being Element of L such that
A6: e = {p} "/\" () and
A7: p in proj1 D by A5;
{p} "/\" () = { (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 () "/\" () by A1, A7; :: thesis: verum
end;
let q be object ; :: according to TARSKI:def 3 :: thesis: ( not q in () "/\" () or q in union { X where X is non empty directed Subset of L : ex x being Element of L st
( X = {x} "/\" () & x in proj1 D )
}
)

assume q in () "/\" () ; :: thesis: q in union { X where X is non empty directed Subset of L : ex x being Element of L st
( X = {x} "/\" () & 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} "/\" () in { X where X is non empty directed Subset of L : S1[X] } by A9;
{x} "/\" () = { (x "/\" d) where d is Element of L : d in proj2 D } by YELLOW_4:42;
then q in {x} "/\" () by ;
hence q in union { X where X is non empty directed Subset of L : ex x being Element of L st
( X = {x} "/\" () & x in proj1 D )
}
by ; :: thesis: verum