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 A2: ( o1 ~= o2 & the_arity_of o1 <= the_arity_of o2 & the_result_sort_of o1 <= the_result_sort_of o2 ) by Def22;
A3: ( o2 ~= o3 & the_arity_of o2 <= the_arity_of o3 & the_result_sort_of o2 <= the_result_sort_of o3 ) by A1, Def22;
hence o1 ~= o3 by A2, Th2; :: according to OSALG_1:def 22 :: thesis: ( the_arity_of o1 <= the_arity_of o3 & the_result_sort_of o1 <= the_result_sort_of o3 )
thus the_arity_of o1 <= the_arity_of o3 by A2, A3, Th21; :: thesis: the_result_sort_of o1 <= the_result_sort_of o3
thus the_result_sort_of o1 <= the_result_sort_of o3 by A2, A3, ORDERS_2:26; :: thesis: verum