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