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