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

proof

assume x = (x1 + x2) + x3 ; :: thesis: x - x1 = x2 + x3
then x = x1 + (x2 + x3) by RVSUM_1:15;
hence x - x1 = x2 + x3 by Th6; :: thesis: verum

end;

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

assume x - x1 = x2 + x3 ; :: thesis: x = (x1 + x2) + x3
hence x = x1 + (x2 + x3) by Th6
.= (x1 + x2) + x3 by RVSUM_1:15 ;
:: thesis: verum

end;

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