let S be OrderSortedSign; :: thesis: for o1, o2, o3 being OperSymbol of S st o1 <= o2 & o2 <= o3 holds
o1 <= o3
let o1, o2, o3 be OperSymbol of S; :: thesis: ( o1 <= o2 & o2 <= o3 implies o1 <= o3 )
assume A1: ( o1 <= o2 & o2 <= o3 ) ; :: thesis: o1 <= o3
then ( o1 ~= o2 & o2 ~= o3 ) by Def22;
hence o1 ~= o3 by Th2; :: according to OSALG_1:def 20 :: thesis: ( the_arity_of o1 <= the_arity_of o3 & the_result_sort_of o1 <= the_result_sort_of o3 )
( the_arity_of o1 <= the_arity_of o2 & the_arity_of o2 <= the_arity_of o3 ) by A1, Def22;
hence the_arity_of o1 <= the_arity_of o3 by Th21; :: thesis: the_result_sort_of o1 <= the_result_sort_of o3
( the_result_sort_of o1 <= the_result_sort_of o2 & the_result_sort_of o2 <= the_result_sort_of o3 ) by A1, Def22;
hence the_result_sort_of o1 <= the_result_sort_of o3 by ORDERS_2:3; :: thesis: verum