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