set US = { F where F is Filter of BL : F is being_ultrafilter } ;
consider p1, p2 being Element of BL such that
A1: p1 <> p2 by STRUCT_0:def 10;
( p1 <> Bottom BL or p2 <> Bottom BL ) by A1;
then consider p being Element of BL such that
A2: p <> Bottom BL ;
consider H being Filter of BL such that
p in H and
A3: H is being_ultrafilter by A2, FILTER_0:20;
H in { F where F is Filter of BL : F is being_ultrafilter } by A3;
hence not ultraset BL is empty ; :: thesis: verum