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

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