let n be Nat; :: thesis: for x1, x2, x3 being Element of REAL n
for L being Element of line_of_REAL n st x1 in L & x2 in L & x3 in L & x1 <> x2 holds
ex a being Real st x3 - x1 = a * (x2 - x1)
let x1, x2, x3 be Element of REAL n; :: thesis: for L being Element of line_of_REAL n st x1 in L & x2 in L & x3 in L & x1 <> x2 holds
ex a being Real st x3 - x1 = a * (x2 - x1)
let L be Element of line_of_REAL n; :: thesis: ( x1 in L & x2 in L & x3 in L & x1 <> x2 implies ex a being Real st x3 - x1 = a * (x2 - x1) )
assume ( x1 in L & x2 in L & x3 in L & x1 <> x2 ) ; :: thesis: ex a being Real st x3 - x1 = a * (x2 - x1)
then ( x1 in Line (x1,x2) & x3 in Line (x1,x2) ) by Th64;
then consider a being Real such that
A1: x3 - x1 = a * (x2 - x1) by Th31;
take a ; :: thesis: x3 - x1 = a * (x2 - x1)
thus x3 - x1 = a * (x2 - x1) by A1; :: thesis: verum