:: deftheorem defines being_ultrafilter FILTER_0:def 3 :
for L being Lattice
for F being Filter of L holds
( F is being_ultrafilter iff ( F <> the carrier of L & ( for H being Filter of L st F c= H & H <> the carrier of L holds
F = H ) ) );