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