theorem Th31: :: NUMBERS:31

REAL c= ExtREAL by XBOOLE_1:7;