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
latt (L,(.p.>) = (latt ((L .:),((.p.> .:))) .: by Th70
.= (latt ((L .:),<.(p .:).))) .: by Th29
.= (latt <.(p .:).)) .: by Th69 ;
hence Top (latt (L,(.p.>)) = Bottom (latt <.(p .:).)) by LATTICE2:61
.= p by FILTER_0:56 ;
:: thesis: verum