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 S1[ 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 : S1[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 }
proof
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 : S1[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 : S1[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 : S1[X] } by A1; :: thesis: verum
end;
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
( 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 : S1[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 & S1[X] ) ;
hence q in { (sup ({x} "/\" (proj2 D))) where x is Element of L : x in proj1 D } ; :: thesis: verum