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

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