theorem Th16: :: ARYTM_0:16

for x being Element of REAL holds * (x,x) in REAL+