for n being Nat
for x1, x2, x3 being Element of REAL n st x1 // x2 & x2 // x3 holds
x1 // x3