theorem Th1: :: NUMBERS:1

REAL c< COMPLEX