for r, s being Real st 0 <= r & 0 <= s & r ^2 = s ^2 holds
r = s