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:49;
then A2: <.(L .:).) = <.(Bottom (L .:)).) by FILTER_0:17;
Bottom (L .:) = (Top L) .: by A1, LATTICE2:62;
hence (.L.> = (.(Top L).> by A2, Th29; :: thesis: verum