theorem :: OSALG_1:23

for S being OrderSortedSign
for o1, o2, o3 being OperSymbol of S st o1 <= o2 & o2 <= o3 holds
o1 <= o3 by Th2, Th21, ORDERS_2:3;