let n be Nat; 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; ( x1 = x2 + x3 iff x2 = x1 - x3 )
thus
( x1 = x2 + x3 implies x2 = x1 - x3 )
( x2 = x1 - x3 implies x1 = x2 + x3 )
now ( x2 = x1 - x3 implies x2 + x3 = x1 )end;
hence
( x2 = x1 - x3 implies x1 = x2 + x3 )
; verum