theorem Th4: :: REALSET3:4

for F being Field
for a, b, c, d being Element of F holds
( a - b = c - d iff a + d = b + c )