theorem Th19: :: NUMBERS:19

NAT c= REAL by Th9;