theorem :: NUMBERS:21

REAL <> COMPLEX by Th1;