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} "/\" (proj2 D) & 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} "/\" (proj2 D) & x in proj1 D ) } ,L
reconsider D1 = proj1 D, D2 = proj2 D as non empty directed Subset of L by YELLOW_3:21, YELLOW_3:22;
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} "/\" (proj2 D) & x in proj1 D ) } ,L by WAYBEL_0:75; :: thesis: verum