A1: ( 0 * p2 = 0. (TOP-REAL n) & p1 + (0. (TOP-REAL n)) = p1 ) by EUCLID:31, EUCLID:33;
( 1 - 0 = 1 & 1 * p1 = p1 ) by EUCLID:33;
then p1 in Line (p1,p2) by A1;
hence not Line (p1,p2) is empty ; :: thesis: verum