let S be OrderSortedSign; :: thesis: for o1, o2 being OperSymbol of S st o1 <= o2 & o2 <= o1 holds
o1 = o2
let o1, o2 be OperSymbol of S; :: thesis: ( o1 <= o2 & o2 <= o1 implies o1 = o2 )
assume A1: ( o1 <= o2 & o2 <= o1 ) ; :: thesis: o1 = o2
then A2: ( o1 ~= o2 & the_arity_of o1 <= the_arity_of o2 & the_result_sort_of o1 <= the_result_sort_of o2 ) by Def22;
( o2 ~= o1 & the_arity_of o2 <= the_arity_of o1 & the_result_sort_of o2 <= the_result_sort_of o1 ) by A1, Def22;
then ( the_arity_of o1 = the_arity_of o2 & the_result_sort_of o1 = the_result_sort_of o2 ) by A2, Th6, ORDERS_2:25;
hence o1 = o2 by A2, Def4; :: thesis: verum