let n be Nat; :: thesis: for x1, x2 being Element of REAL n holds

( x1 in Line (x1,x2) & x2 in Line (x1,x2) )

let x1, x2 be Element of REAL n; :: thesis: ( x1 in Line (x1,x2) & x2 in Line (x1,x2) )

A1: ( 1 - 0 = 1 & 1 * x1 = x1 ) by Th3;

A2: ( 1 - 1 = 0 & 0 * x1 = 0* n ) by Th3;

A3: ( 1 * x2 = x2 & (0* n) + x2 = x2 ) by Th1, Th3;

( 0 * x2 = 0* n & x1 + (0* n) = x1 ) by Th1, Th3;

hence ( x1 in Line (x1,x2) & x2 in Line (x1,x2) ) by A1, A2, A3; :: thesis: verum

( x1 in Line (x1,x2) & x2 in Line (x1,x2) )

let x1, x2 be Element of REAL n; :: thesis: ( x1 in Line (x1,x2) & x2 in Line (x1,x2) )

A1: ( 1 - 0 = 1 & 1 * x1 = x1 ) by Th3;

A2: ( 1 - 1 = 0 & 0 * x1 = 0* n ) by Th3;

A3: ( 1 * x2 = x2 & (0* n) + x2 = x2 ) by Th1, Th3;

( 0 * x2 = 0* n & x1 + (0* n) = x1 ) by Th1, Th3;

hence ( x1 in Line (x1,x2) & x2 in Line (x1,x2) ) by A1, A2, A3; :: thesis: verum