theorem Th2: :: ARYTM_0:2

for x being Element of REAL+ st x <> {} holds
[{},x] in REAL