for BL being non trivial B_Lattice
for a being Element of BL
for F being Filter of BL st F is being_ultrafilter & not F in (UFilter BL) . a holds
not a in F by Th18;