let L be Lattice; :: thesis: for p being Element of st ex r being Element of st p "/\" r <> p holds
<.p.) <> the carrier of L
let p be Element of ; :: thesis: ( ex r being Element of st p "/\" r <> p implies <.p.) <> the carrier of L )
given r being Element of such that A1: p "/\" r <> p ; :: thesis: <.p.) <> the carrier of L
p "/\" r [= p by LATTICES:23;
then not p [= p "/\" r by A1, LATTICES:26;
hence <.p.) <> the carrier of L by Th18; :: thesis: verum