theorem :: FILTER_0:45

for B being B_Lattice
for FB being Filter of B holds
( ( FB <> <.B.) & FB is prime ) iff FB is being_ultrafilter )