:: deftheorem defines ultraset LOPCLSET:def 5 :
for BL being non trivial B_Lattice holds ultraset BL = { F where F is Filter of BL : F is being_ultrafilter } ;