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