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 Th29, Th36;
hence ( D = {p} implies (.D.> = (.p.> ) by FILTER_0:24; :: thesis: verum