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