let n be Nat; :: thesis: for x1, x2 being Element of REAL n holds
( x1 = x2 iff x1 - x2 = 0* n )
let x1, x2 be Element of REAL n; :: thesis: ( x1 = x2 iff x1 - x2 = 0* n )
thus ( x1 = x2 implies x1 - x2 = 0* n ) by Th2; :: thesis: ( x1 - x2 = 0* n implies x1 = x2 )
assume x1 - x2 = 0* n ; :: thesis: x1 = x2
hence x1 = x2 + (0* n) by Th6
.= x2 by EUCLID_4:1 ;
:: thesis: verum