theorem Th5: :: ARYTM_0:5

REAL+ misses [:{{}},REAL+:]