:: deftheorem defines principal CARD_FIL:def 6 :
for X being non empty set
for F being Filter of X holds
( F is principal iff ex Y being Subset of X st
( Y in F & ( for Z being Subset of X st Z in F holds
Y c= Z ) ) );