let AS be AffinSpace; for a, b being Element of AS holds Line (a,b) c= Line (b,a)
let a, b be Element of AS; Line (a,b) c= Line (b,a)
let x be object ; TARSKI:def 3 ( not x in Line (a,b) or x in Line (b,a) )
assume A1:
x in Line (a,b)
; x in Line (b,a)
then reconsider x9 = x as Element of AS ;
LIN a,b,x9
by A1, Def2;
then
LIN b,a,x9
by Th5;
hence
x in Line (b,a)
by Def2; verum