let L be Lattice; :: thesis: for p being Element of L
for D being non empty Subset of L st p in D holds
(.p.> c= (.D.>
let p be Element of L; :: thesis: for D being non empty Subset of L st p in D holds
(.p.> c= (.D.>
let D be non empty Subset of L; :: thesis: ( p in D implies (.p.> c= (.D.> )
( p = p .: & <.(p .: ).) = (.p.> & D = D .: & <.(D .: ).) = (.D.> ) by Th30, Th37;
hence ( p in D implies (.p.> c= (.D.> ) by FILTER_0:29; :: thesis: verum