let a, b be Element of AS; :: thesis: Line (a,b) = Line (b,a)
A1: Line (b,a) c= Line (a,b) by Lm5;
Line (a,b) c= Line (b,a) by Lm5;
hence Line (a,b) = Line (b,a) by A1, XBOOLE_0:def 10; :: thesis: verum