let n be Nat; :: thesis: for q1, p1, p2, q2 being Point of (TOP-REAL n) st q1 in Line p1,p2 & q2 in Line p1,p2 holds
Line q1,q2 c= Line p1,p2
let q1, p1, p2, q2 be Point of (TOP-REAL n); :: thesis: ( q1 in Line p1,p2 & q2 in Line p1,p2 implies Line q1,q2 c= Line p1,p2 )
assume A1: ( q1 in Line p1,p2 & q2 in Line p1,p2 ) ; :: thesis: Line q1,q2 c= Line p1,p2
( ex x1, x2 being Element of REAL n st
( x1 = p1 & x2 = p2 & Line x1,x2 = Line p1,p2 ) & ex y1, y2 being Element of REAL n st
( y1 = q1 & y2 = q2 & Line y1,y2 = Line q1,q2 ) ) by Lm8;
hence Line q1,q2 c= Line p1,p2 by A1, Th11; :: thesis: verum