theorem Th17: :: CARD_FIL:17

for X being non empty set
for F being Filter of X ex Uf being Filter of X st
( F c= Uf & Uf is being_ultrafilter )