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 & D .: = D ) by LATTICE2:64, LATTICE2:79;
assume Top L in D ; :: thesis: ( (.D.> = (.L.> & (.D.> = the carrier of L )
then ( <.(D .: ).) = <.(L .: ).) & <.(D .: ).) = H₁(L .: ) & H₁(L .: ) = H₁(L) & <.(D .: ).) = (.D.> ) by A1, Th37, FILTER_0:31;
hence ( (.D.> = (.L.> & (.D.> = the carrier of L ) ; :: thesis: verum