let n be Nat; 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; ( x = (x1 + x2) + x3 iff x - x1 = x2 + x3 )
thus
( x = (x1 + x2) + x3 implies x - x1 = x2 + x3 )
( x - x1 = x2 + x3 implies x = (x1 + x2) + x3 )
now ( x - x1 = x2 + x3 implies x = (x1 + x2) + x3 )assume
x - x1 = x2 + x3
;
x = (x1 + x2) + x3hence x =
x1 + (x2 + x3)
by Th6
.=
(x1 + x2) + x3
by RVSUM_1:15
;
verum end;
hence
( x - x1 = x2 + x3 implies x = (x1 + x2) + x3 )
; verum