let AS be AffinSpace; :: thesis: for a, b being Element of holds Line a,b c= Line b,a
let a, b be Element of ; :: thesis: Line a,b c= Line b,a

now

let x be set ; :: thesis: ( x in Line a,b implies x in Line b,a )
assume A1: x in Line a,b ; :: thesis: x in Line b,a
then reconsider x' = x as Element of ;
LIN a,b,x' by A1, Def2;
then LIN b,a,x' by Th15;
hence x in Line b,a by Def2; :: thesis: verum

end;

hence Line a,b c= Line b,a by TARSKI:def 3; :: thesis: verum