let n be Element of NAT ; :: thesis: for x1, x2, x3 being Element of REAL n st x1 // x2 & x2 // x3 holds
x1 // x3
let x1, x2, x3 be Element of REAL n; :: thesis: ( x1 // x2 & x2 // x3 implies x1 // x3 )
assume A1: ( x1 // x2 & x2 // x3 ) ; :: thesis: x1 // x3
then A2: ( x1 <> 0* n & x2 <> 0* n & ex r being Real st x1 = r * x2 ) by Def1;
A3: ( x2 <> 0* n & x3 <> 0* n & ex s being Real st x2 = s * x3 ) by A1, Def1;
ex t being Real st x1 = t * x3

proof

consider a being Real such that
A4: x1 = a * x2 by A1, Def1;
consider b being Real such that
A5: x2 = b * x3 by A1, Def1;
x1 = (a * b) * x3 by A4, A5, EUCLID_4:4;
hence ex t being Real st x1 = t * x3 ; :: thesis: verum

end;

hence x1 // x3 by A2, A3, Def1; :: thesis: verum