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