theorem :: JORDAN18:1

for a, b being Real holds (a - b) ^2 = (b - a) ^2 ;