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