let BL be non trivial B_Lattice; :: thesis: (UFilter BL) . (Bottom BL) = {}
assume A1: (UFilter BL) . (Bottom BL) <> {} ; :: thesis: contradiction
set x = the Element of (UFilter BL) . (Bottom BL);
ex F being Filter of BL st
( F = the Element of (UFilter BL) . (Bottom BL) & F is being_ultrafilter & Bottom BL in F ) by A1, Th17;
hence contradiction by Th29; :: thesis: verum