theorem Th5: :: CARD_4:5

( [:NAT,NAT:], NAT are_equipotent & card NAT = card [:NAT,NAT:] )