A1: ( 1 - 0 = 1 & 1 * x1 = x1 ) by Th3;
( 0 * x2 = 0* n & x1 + (0* n) = x1 ) by Th1, Th3;
then x1 in Line (x1,x2) by A1;
hence not Line (x1,x2) is empty ; :: thesis: verum