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:49, LATTICE3:50;
hence L is bounded ; :: thesis: verum