theorem :: EUCLID_8:28

for p being Element of REAL 3 holds 1 * p = p by RFUNCT_1:21;