theorem Th23: :: CARD_FIL:23

for X being infinite set
for F being Filter of X st not F is principal & F is being_ultrafilter & F is_complete_with card X holds
F is uniform