let t be Real; :: thesis: for n being Nat
for x0, x, x1 being Element of REAL n st x1 - x0 = t * x & x1 <> x0 holds
t <> 0
let n be Nat; :: thesis: for x0, x, x1 being Element of REAL n st x1 - x0 = t * x & x1 <> x0 holds
t <> 0
let x0, x, x1 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, Th9; :: thesis: verum