let L be Lattice; :: thesis: for p being Element of L holds Top (latt L,(.p.>) = p
let p be Element of L; :: thesis: Top (latt L,(.p.>) = p
A1: latt <.(p .: ).) is lower-bounded by FILTER_0:70;
latt L,(.p.> = (latt (L .: ),((.p.> .: )) .: by Th71
.= (latt (L .: ),<.(p .: ).)) .: by Th30
.= (latt <.(p .: ).)) .: by Th70 ;
hence Top (latt L,(.p.>) = Bottom (latt <.(p .: ).)) by A1, LATTICE2:78
.= p by FILTER_0:71 ;
:: thesis: verum