:: deftheorem Def7 defines being_ultrafilter CARD_FIL:def 7 :
for X being non empty set
for F being Filter of X holds
( F is being_ultrafilter iff for Y being Subset of X holds
( Y in F or X \ Y in F ) );