let L be Lattice; :: thesis: ( L is upper-bounded implies (.L.> = (.(Top L).> )
assume L is upper-bounded ; :: thesis: (.L.> = (.(Top L).>
then ( L .: is lower-bounded & Top L = Bottom (L .: ) ) by LATTICE2:64, LATTICE2:79;
then ( <.(L .: ).) = <.(Bottom (L .: )).) & <.(L .: ).) = H₁(L .: ) & H₁(L .: ) = H₁(L) & (.L.> = H₁(L) & Bottom (L .: ) = (Top L) .: ) by FILTER_0:20;
hence (.L.> = (.(Top L).> by Th30; :: thesis: verum