let L be up-complete Semilattice; :: thesis: for D being non empty directed Subset of [:L,L:] holds "\/" ( { (sup X) where X is non empty directed Subset of L : ex x being Element of L st
( X = {x} "/\" () & x in proj1 D )
}
,L) = "\/" ((union { X where X is non empty directed Subset of L : ex x being Element of L st
( X = {x} "/\" () & x in proj1 D )
}
)
,L)

let D be non empty directed Subset of [:L,L:]; :: thesis: "\/" ( { (sup X) where X is non empty directed Subset of L : ex x being Element of L st
( X = {x} "/\" () & x in proj1 D )
}
,L) = "\/" ((union { X where X is non empty directed Subset of L : ex x being Element of L st
( X = {x} "/\" () & x in proj1 D )
}
)
,L)

defpred S1[ set ] means ex x being Element of L st
( \$1 = {x} "/\" () & x in proj1 D );
A1: "\/" ( { (sup X) where X is non empty directed Subset of L : S1[X] } ,L) <= "\/" ((union { X where X is non empty directed Subset of L : S1[X] } ),L) by Th9;
A2: union { X where X is non empty directed Subset of L : S1[X] } is_<=_than "\/" ( { ("\/" (X,L)) where X is non empty directed Subset of L : S1[X] } ,L)
proof
let a be Element of L; :: according to LATTICE3:def 9 :: thesis: ( not a in union { X where X is non empty directed Subset of L : S1[X] } or a <= "\/" ( { ("\/" (X,L)) where X is non empty directed Subset of L : S1[X] } ,L) )
assume a in union { X where X is non empty directed Subset of L : S1[X] } ; :: thesis: a <= "\/" ( { ("\/" (X,L)) where X is non empty directed Subset of L : S1[X] } ,L)
then consider b being set such that
A3: a in b and
A4: b in { X where X is non empty directed Subset of L : S1[X] } by TARSKI:def 4;
consider c being non empty directed Subset of L such that
A5: b = c and
A6: S1[c] by A4;
"\/" (c,L) in { ("\/" (X,L)) where X is non empty directed Subset of L : S1[X] } by A6;
then A7: "\/" (c,L) <= "\/" ( { ("\/" (X,L)) where X is non empty directed Subset of L : S1[X] } ,L) by ;
ex_sup_of c,L by WAYBEL_0:75;
then a <= "\/" (c,L) by ;
hence a <= "\/" ( { ("\/" (X,L)) where X is non empty directed Subset of L : S1[X] } ,L) by ; :: thesis: verum
end;
ex_sup_of union { X where X is non empty directed Subset of L : S1[X] } ,L by Th7;
then "\/" ((union { X where X is non empty directed Subset of L : S1[X] } ),L) <= "\/" ( { ("\/" (X,L)) where X is non empty directed Subset of L : S1[X] } ,L) by ;
hence "\/" ( { (sup X) where X is non empty directed Subset of L : ex x being Element of L st
( X = {x} "/\" () & x in proj1 D )
}
,L) = "\/" ((union { X where X is non empty directed Subset of L : ex x being Element of L st
( X = {x} "/\" () & x in proj1 D )
}
)
,L) by ; :: thesis: verum