let t be Real; :: thesis: for n being Element of NAT
for x1, x0, x being Element of REAL n st x1 - x0 = t * x & x1 <> x0 holds
t <> 0
let n be Element of NAT ; :: thesis: for x1, x0, x being Element of REAL n st x1 - x0 = t * x & x1 <> x0 holds
t <> 0
let x1, x0, x be Element of REAL n; :: thesis: ( x1 - x0 = t * x & x1 <> x0 implies t <> 0 )
assume that
A1: x1 - x0 = t * x and
A2: x1 <> x0 ; :: thesis: t <> 0
assume not t <> 0 ; :: thesis: contradiction
then x1 - x0 = 0* n by A1, EUCLID_4:3;
hence contradiction by A2, Th14; :: thesis: verum