:: deftheorem defines uniform CARD_FIL:def 5 :
for X being non empty set
for F being Filter of X holds
( F is uniform iff for Y being Subset of X st Y in F holds
card Y = card X );