let L be Lattice; :: thesis: for p being Element of L holds latt <.p.) is lower-bounded
let p be Element of L; :: thesis: latt <.p.) is lower-bounded
the carrier of (latt <.p.)) = <.p.) by Th63;
then reconsider p9 = p as Element of (latt <.p.)) by Th19;
take p9 ; :: according to LATTICES:def 13 :: thesis: for b₁ being Element of the carrier of (latt <.p.)) holds
( p9 "/\" b₁ = p9 & b₁ "/\" p9 = p9 )
let q9 be Element of (latt <.p.)); :: thesis: ( p9 "/\" q9 = p9 & q9 "/\" p9 = p9 )
reconsider q = q9 as Element of <.p.) by Th63;
p [= q by Th18;
then p "/\" q = p by LATTICES:21;
hence ( p9 "/\" q9 = p9 & q9 "/\" p9 = p9 ) by Th64; :: thesis: verum