theorem Th1: :: COUNTERS:1

( NAT c< ExtNAT & ExtNAT c< ExtREAL )