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) & q1 <> q2 holds
Line (p1,p2) c= Line (q1,q2)
let q1, p1, p2, q2 be Point of (TOP-REAL n); :: thesis: ( q1 in Line (p1,p2) & q2 in Line (p1,p2) & q1 <> q2 implies Line (p1,p2) c= Line (q1,q2) )
assume A1: ( q1 in Line (p1,p2) & q2 in Line (p1,p2) & q1 <> q2 ) ; :: thesis: Line (p1,p2) c= Line (q1,q2)
( 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 (p1,p2) c= Line (q1,q2) by A1, Th12; :: thesis: verum