let n be Nat; :: thesis: for p1, p2 being Point of (TOP-REAL n) holds Line p1,p2 = Line p2,p1
let p1, p2 be Point of (TOP-REAL n); :: thesis: Line p1,p2 = Line p2,p1
( ex x1, x2 being Element of REAL n st
( x1 = p1 & x2 = p2 & Line x1,x2 = Line p1,p2 ) & ex x29, x19 being Element of REAL n st
( x29 = p2 & x19 = p1 & Line x29,x19 = Line p2,p1 ) ) by Lm8;
hence Line p1,p2 = Line p2,p1 ; :: thesis: verum