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 set ; :: 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