for n being Nat
for a, b, c being Element of REAL n st a < b & b < c holds
a < c