theorem Th2: :: GOBOARD7:2

for r, s being Real holds
( |.(r - s).| = 0 iff r = s )