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

( 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

( 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

then reconsider S = union { X where X is non empty directed Subset of L : ex x being Element of L st
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;( 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

( 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