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