let BL be non trivial B_Lattice; :: thesis: (UFilter BL) . (Top BL) = ultraset BL
thus (UFilter BL) . (Top BL) = (UFilter BL) . ((Bottom BL) `) by LATTICE4:30
.= (ultraset BL) \ ((UFilter BL) . (Bottom BL)) by Th25
.= (ultraset BL) \ {} by Th30
.= ultraset BL ; :: thesis: verum