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