let L be Lattice; :: thesis: ( L is complete implies L is bounded )
assume L is complete ; :: thesis: L is bounded
then ( L is 0_Lattice & L is 1_Lattice ) by LATTICE3:50, LATTICE3:51;
hence L is bounded ; :: thesis: verum