theorem Th10: :: WAYBEL22:10

for X being set holds card (FixedUltraFilters X) = card X