let L be up-complete Semilattice; :: thesis: for D being non empty directed Subset of holds { (sup ({x} "/\" (proj2 D))) where x is Element of : x in proj1 D } = { (sup X) where X is non empty directed Subset of : ex x being Element of st
( X = {x} "/\" (proj2 D) & x in proj1 D ) }
let D be non empty directed Subset of ; :: thesis: { (sup ({x} "/\" (proj2 D))) where x is Element of : x in proj1 D } = { (sup X) where X is non empty directed Subset of : ex x being Element of st
( X = {x} "/\" (proj2 D) & x in proj1 D ) }
defpred S₁[ set ] means ex x being Element of st
( $1 = {x} "/\" (proj2 D) & x in proj1 D );
reconsider D1 = proj1 D, D2 = proj2 D as non empty directed Subset of by YELLOW_3:21, YELLOW_3:22;
thus { (sup ({x} "/\" (proj2 D))) where x is Element of : x in proj1 D } c= { (sup X) where X is non empty directed Subset of : S₁[X] } :: according to XBOOLE_0:def 10 :: thesis: { (sup X) where X is non empty directed Subset of : ex x being Element of st
( X = {x} "/\" (proj2 D) & x in proj1 D ) } c= { (sup ({x} "/\" (proj2 D))) where x is Element of : x in proj1 D }

proof

let q be set ; :: according to TARSKI:def 3 :: thesis: ( not q in { (sup ({x} "/\" (proj2 D))) where x is Element of : x in proj1 D } or q in { (sup X) where X is non empty directed Subset of : S₁[X] } )
assume q in { (sup ({x} "/\" (proj2 D))) where x is Element of : x in proj1 D } ; :: thesis: q in { (sup X) where X is non empty directed Subset of : S₁[X] }
then consider x being Element of such that
A1: ( q = sup ({x} "/\" D2) & x in D1 ) ;
reconsider xx = {x} as non empty directed Subset of 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 : S₁[X] } by A1; :: thesis: verum

end;

let q be set ; :: according to TARSKI:def 3 :: thesis: ( not q in { (sup X) where X is non empty directed Subset of : ex x being Element of st
( X = {x} "/\" (proj2 D) & x in proj1 D ) } or q in { (sup ({x} "/\" (proj2 D))) where x is Element of : x in proj1 D } )
assume q in { (sup X) where X is non empty directed Subset of : S₁[X] } ; :: thesis: q in { (sup ({x} "/\" (proj2 D))) where x is Element of : x in proj1 D }
then ex X being non empty directed Subset of st
( q = sup X & S₁[X] ) ;
hence q in { (sup ({x} "/\" (proj2 D))) where x is Element of : x in proj1 D } ; :: thesis: verum