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