let n be Nat; :: thesis: for x1, x2, x3 being Element of REAL n holds
( x1 = x2 + x3 iff x2 = x1 - x3 )
let x1, x2, x3 be Element of REAL n; :: thesis: ( x1 = x2 + x3 iff x2 = x1 - x3 )
thus ( x1 = x2 + x3 implies x2 = x1 - x3 ) :: thesis: ( x2 = x1 - x3 implies x1 = x2 + x3 )

proof

assume x1 = x2 + x3 ; :: thesis: x2 = x1 - x3
hence x1 - x3 = x2 + (x3 + (- x3)) by RVSUM_1:15
.= x2 + (0* n) by Th2
.= x2 by EUCLID_4:1 ;
:: thesis: verum

end;

now :: thesis: ( x2 = x1 - x3 implies x2 + x3 = x1 )

assume x2 = x1 - x3 ; :: thesis: x2 + x3 = x1
hence x2 + x3 = x1 + ((- x3) + x3) by RVSUM_1:15
.= x1 + (0* n) by Th2
.= x1 by EUCLID_4:1 ;
:: thesis: verum

end;

hence ( x2 = x1 - x3 implies x1 = x2 + x3 ) ; :: thesis: verum