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 .:) ;
then <.(p .:).) <> H₁(L .: ) by A1, FILTER_0:19;
hence (.p.> <> the carrier of L by Th29; :: thesis: verum