theorem Th8: :: CARD_5:8

for A being Ordinal ex B being Ordinal st
( B c= card A & A is_cofinal_with B )