theorem Th15: :: EUCLID:18

for n being Nat
for x1, x2 being Element of REAL n holds |.(x1 - x2).| = |.(x2 - x1).|