theorem :: EUCLID:25

for n being Nat
for x being Element of REAL n holds sqr (abs x) = sqr x by Lm2;