theorem Th1: :: WSIERP_1:1

for x being Real holds
( x |^ 2 = x * x & (- x) |^ 2 = x |^ 2 )