let L be Lattice; :: thesis: for D being non empty Subset of L st L is upper-bounded & Top L in D holds
( (.D.> = (.L.> & (.D.> = the carrier of L )
let D be non empty Subset of L; :: thesis: ( L is upper-bounded & Top L in D implies ( (.D.> = (.L.> & (.D.> = the carrier of L ) )
assume L is upper-bounded ; :: thesis: ( not Top L in D or ( (.D.> = (.L.> & (.D.> = the carrier of L ) )
then A1: ( L .: is lower-bounded & Bottom (L .: ) = Top L ) by LATTICE2:64, LATTICE2:79;
assume Top L in D ; :: thesis: ( (.D.> = (.L.> & (.D.> = the carrier of L )
then <.(D .: ).) = <.(L .: ).) by A1, FILTER_0:31;
hence ( (.D.> = (.L.> & (.D.> = the carrier of L ) by Th37; :: thesis: verum