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