let L be Lattice; :: thesis: for p being Element of L st L is 1_Lattice holds
latt <.p.) is bounded
let p be Element of L; :: thesis: ( L is 1_Lattice implies latt <.p.) is bounded )
assume L is 1_Lattice ; :: thesis: latt <.p.) is bounded
hence ( latt <.p.) is lower-bounded & latt <.p.) is upper-bounded ) by Th66, Th70; :: according to LATTICES:def 15 :: thesis: verum