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 .: ) "/\" (r .: ) & p = p .: ) ;
then ( <.(p .: ).) <> H₁(L .: ) & H₁(L .: ) = H₁(L) ) by A1, FILTER_0:23;
hence (.p.> <> the carrier of L by Th30; :: thesis: verum