let L be up-complete Semilattice; :: thesis: for D being non empty directed Subset of [:L,L:] holds ex_sup_of union { X where X is non empty directed Subset of L : ex x being Element of L st
( X = {x} "/\" () & x in proj1 D )
}
,L

let D be non empty directed Subset of [:L,L:]; :: thesis: ex_sup_of union { X where X is non empty directed Subset of L : ex x being Element of L st
( X = {x} "/\" () & x in proj1 D )
}
,L

reconsider D1 = proj1 D, D2 = proj2 D as non empty directed Subset of L by ;
set A = { X where X is non empty directed Subset of L : ex x being Element of L st
( X = {x} "/\" D2 & x in D1 )
}
;
union { X where X is non empty directed Subset of L : ex x being Element of L st
( X = {x} "/\" D2 & x in D1 )
}
c= the carrier of L
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 : ex x being Element of L st
( X = {x} "/\" D2 & x in D1 )
}
or q in the carrier of L )

assume q in union { X where X is non empty directed Subset of L : ex x being Element of L st
( X = {x} "/\" D2 & x in D1 )
}
; :: thesis: q in the carrier of L
then consider r being set such that
A1: q in r and
A2: r in { X where X is non empty directed Subset of L : ex x being Element of L st
( X = {x} "/\" D2 & x in D1 )
}
by TARSKI:def 4;
ex s being non empty directed Subset of L st
( r = s & ex x being Element of L st
( s = {x} "/\" D2 & x in D1 ) ) by A2;
hence q in the carrier of L by A1; :: thesis: verum
end;
then reconsider S = union { X where X is non empty directed Subset of L : ex x being Element of L st
( X = {x} "/\" D2 & x in D1 )
}
as Subset of L ;
S = D1 "/\" D2 by Th6;
hence ex_sup_of union { X where X is non empty directed Subset of L : ex x being Element of L st
( X = {x} "/\" () & x in proj1 D )
}
,L by WAYBEL_0:75; :: thesis: verum