theorem :: SRINGS_5:69

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