:: deftheorem Def6 defines UFilter LOPCLSET:def 6 :
for BL being non trivial B_Lattice
for b₂ being Function holds
( b₂ = UFilter BL iff ( dom b₂ = the carrier of BL & ( for a being Element of BL holds b₂ . a = { UF where UF is Filter of BL : ( UF is being_ultrafilter & a in UF ) } ) ) );