let L be up-complete Semilattice; :: thesis: for D being non empty directed Subset of [:L,L:] holds { (sup ({x} "/\" (proj2 D))) where x is Element of L : x in proj1 D } = { (sup 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 ) }

let D be non empty directed Subset of [:L,L:]; :: thesis: { (sup ({x} "/\" (proj2 D))) where x is Element of L : x in proj1 D } = { (sup 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 ) }

defpred S_{1}[ set ] means ex x being Element of L st

( $1 = {x} "/\" (proj2 D) & x in proj1 D );

reconsider D1 = proj1 D, D2 = proj2 D as non empty directed Subset of L by YELLOW_3:21, YELLOW_3:22;

thus { (sup ({x} "/\" (proj2 D))) where x is Element of L : x in proj1 D } c= { (sup X) where X is non empty directed Subset of L : S_{1}[X] }
:: according to XBOOLE_0:def 10 :: thesis: { (sup 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 ) } c= { (sup ({x} "/\" (proj2 D))) where x is Element of L : x in proj1 D }

( X = {x} "/\" (proj2 D) & x in proj1 D ) } or q in { (sup ({x} "/\" (proj2 D))) where x is Element of L : x in proj1 D } )

assume q in { (sup X) where X is non empty directed Subset of L : S_{1}[X] }
; :: thesis: q in { (sup ({x} "/\" (proj2 D))) where x is Element of L : x in proj1 D }

then ex X being non empty directed Subset of L st

( q = sup X & S_{1}[X] )
;

hence q in { (sup ({x} "/\" (proj2 D))) where x is Element of L : x in proj1 D } ; :: thesis: verum

( X = {x} "/\" (proj2 D) & x in proj1 D ) }

let D be non empty directed Subset of [:L,L:]; :: thesis: { (sup ({x} "/\" (proj2 D))) where x is Element of L : x in proj1 D } = { (sup 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 ) }

defpred S

( $1 = {x} "/\" (proj2 D) & x in proj1 D );

reconsider D1 = proj1 D, D2 = proj2 D as non empty directed Subset of L by YELLOW_3:21, YELLOW_3:22;

thus { (sup ({x} "/\" (proj2 D))) where x is Element of L : x in proj1 D } c= { (sup X) where X is non empty directed Subset of L : S

( X = {x} "/\" (proj2 D) & x in proj1 D ) } c= { (sup ({x} "/\" (proj2 D))) where x is Element of L : x in proj1 D }

proof

let q be object ; :: according to TARSKI:def 3 :: thesis: ( not q in { (sup 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 { (sup ({x} "/\" (proj2 D))) where x is Element of L : x in proj1 D } or q in { (sup X) where X is non empty directed Subset of L : S_{1}[X] } )

assume q in { (sup ({x} "/\" (proj2 D))) where x is Element of L : x in proj1 D } ; :: thesis: q in { (sup X) where X is non empty directed Subset of L : S_{1}[X] }

then consider x being Element of L such that

A1: ( q = sup ({x} "/\" D2) & x in D1 ) ;

reconsider xx = {x} as non empty directed Subset of L by WAYBEL_0:5;

( not xx "/\" D2 is empty & xx "/\" D2 is directed ) ;

hence q in { (sup X) where X is non empty directed Subset of L : S_{1}[X] }
by A1; :: thesis: verum

end;assume q in { (sup ({x} "/\" (proj2 D))) where x is Element of L : x in proj1 D } ; :: thesis: q in { (sup X) where X is non empty directed Subset of L : S

then consider x being Element of L such that

A1: ( q = sup ({x} "/\" D2) & x in D1 ) ;

reconsider xx = {x} as non empty directed Subset of L by WAYBEL_0:5;

( not xx "/\" D2 is empty & xx "/\" D2 is directed ) ;

hence q in { (sup X) where X is non empty directed Subset of L : S

( X = {x} "/\" (proj2 D) & x in proj1 D ) } or q in { (sup ({x} "/\" (proj2 D))) where x is Element of L : x in proj1 D } )

assume q in { (sup X) where X is non empty directed Subset of L : S

then ex X being non empty directed Subset of L st

( q = sup X & S

hence q in { (sup ({x} "/\" (proj2 D))) where x is Element of L : x in proj1 D } ; :: thesis: verum