let n be Nat; :: thesis: for x1, x2 being Element of REAL n holds Line x1,x2 = Line x2,x1
let x1, x2 be Element of REAL n; :: thesis: Line x1,x2 = Line x2,x1
( Line x1,x2 c= Line x2,x1 & Line x2,x1 c= Line x1,x2 ) by Lm1;
hence Line x1,x2 = Line x2,x1 by XBOOLE_0:def 10; :: thesis: verum