theorem THSD2: :: GTARSKI2:6

for n being Nat
for a, b, c being Element of (TOP-REAL n) st a - c = b - c holds
a = b