theorem Th33: :: EUCLID_4:33

for n being Nat
for x, y being Element of REAL n holds |((x - y),(x - y))| = (|(x,x)| - (2 * |(x,y)|)) + |(y,y)|