theorem Th17: :: LOPCLSET:17

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