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:49, LATTICE2:62;
assume Top L in D ; :: thesis: ( (.D.> = (.L.> & (.D.> = the carrier of L )
then <.(D .:).) = <.(L .:).) by A1, FILTER_0:25;
hence ( (.D.> = (.L.> & (.D.> = the carrier of L ) by Th36; :: thesis: verum