theorem :: LOPCLSET:15

for x being set
for BL being non trivial B_Lattice holds
( x in ultraset BL iff ex UF being Filter of BL st
( UF = x & UF is being_ultrafilter ) ) ;