let AS be AffinSpace; :: thesis: for a, b being Element of AS holds Line a,b = Line b,a
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