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