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.> & <.(D .:).) = (.D.> ) by Th29, Th36;
hence ( p in D implies (.p.> c= (.D.> ) by FILTER_0:23; :: thesis: verum