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:37
.= (ultraset BL) \ ((UFilter BL) . (Bottom BL)) by Th28
.= (ultraset BL) \ {} by Th36
.= ultraset BL ; :: thesis: verum