let F be Field; :: thesis: for a, b, c, d being Element of F holds
( a - b = c - d iff a + d = b + c )
let a, b, c, d be Element of F; :: thesis: ( a - b = c - d iff a + d = b + c )

hereby :: thesis: ( a + d = b + c implies a - b = c - d )

assume a - b = c - d ; :: thesis: a + d = b + c
then (c - d) + b = (a + (- b)) + b
.= a + (b - b) by RLVECT_1:def 3
.= a + (0. F) by RLVECT_1:5
.= a by RLVECT_1:4 ;
hence a + d = ((c + b) + (- d)) + d by RLVECT_1:def 3
.= (c + b) + (d - d) by RLVECT_1:def 3
.= (c + b) + (0. F) by RLVECT_1:5
.= b + c by RLVECT_1:4 ;
:: thesis: verum

end;

assume a + d = b + c ; :: thesis: a - b = c - d
then (b + c) - d = a + (d - d) by RLVECT_1:def 3
.= a + (0. F) by RLVECT_1:5
.= a by RLVECT_1:4 ;
hence a - b = ((c - d) + b) - b by RLVECT_1:def 3
.= (c - d) + (b - b) by RLVECT_1:def 3
.= (c - d) + (0. F) by RLVECT_1:5
.= c - d by RLVECT_1:4 ;
:: thesis: verum