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