theorem :: NUMBERS:25

INT <> REAL by Th2, Th4;