let n be Nat; :: thesis: for x1, x2 being Element of REAL n holds Line (x1,x2) c= Line (x2,x1)

let x1, x2 be Element of REAL n; :: thesis: Line (x1,x2) c= Line (x2,x1)

let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in Line (x1,x2) or z in Line (x2,x1) )

assume z in Line (x1,x2) ; :: thesis: z in Line (x2,x1)

then consider t being Real such that

A1: z = ((1 - t) * x1) + (t * x2) ;

z = ((1 - (1 - t)) * x2) + ((1 - t) * x1) by A1;

hence z in Line (x2,x1) ; :: thesis: verum

let x1, x2 be Element of REAL n; :: thesis: Line (x1,x2) c= Line (x2,x1)

let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in Line (x1,x2) or z in Line (x2,x1) )

assume z in Line (x1,x2) ; :: thesis: z in Line (x2,x1)

then consider t being Real such that

A1: z = ((1 - t) * x1) + (t * x2) ;

z = ((1 - (1 - t)) * x2) + ((1 - t) * x1) by A1;

hence z in Line (x2,x1) ; :: thesis: verum