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

let a, b be Element of AS; :: thesis: Line (a,b) c= Line (b,a)

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Line (a,b) or x in Line (b,a) )

assume A1: x in Line (a,b) ; :: thesis: 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; :: thesis: verum

let a, b be Element of AS; :: thesis: Line (a,b) c= Line (b,a)

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Line (a,b) or x in Line (b,a) )

assume A1: x in Line (a,b) ; :: thesis: 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; :: thesis: verum