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