let x1, x2 be Element of REAL n; :: thesis: ( (n,x1,x2) implies (n,x2,x1) )
assume A1: x1 // x2 ; :: thesis: (n,x2,x1)
then A2: ( x1 <> 0* n & x2 <> 0* n ) ;
consider a being Real such that
A3: a <> 0 and
A4: x1 = a * x2 by A1, Th32;
(1 / a) * x1 = (a / a) * x2 by A4, Th1
.= 1 * x2 by A3, XCMPLX_1:60
.= x2 by EUCLID_4:3 ;
hence (n,x2,x1) by A2; :: thesis: verum