theorem Th1: :: ARYTM_0:1

REAL+ c= REAL