theorem Th18: :: LOPCLSET:18

for BL being non trivial B_Lattice
for a being Element of BL
for F being Filter of BL holds
( F in (UFilter BL) . a iff ( F is being_ultrafilter & a in F ) )