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 that
A1: o1 <= o2 and
A2: o2 <= o1 ; :: thesis: o1 = o2
( the_result_sort_of o1 <= the_result_sort_of o2 & the_result_sort_of o2 <= the_result_sort_of o1 ) by A1, A2;
then A3: the_result_sort_of o1 = the_result_sort_of o2 by ORDERS_2:2;
( the_arity_of o1 <= the_arity_of o2 & the_arity_of o2 <= the_arity_of o1 ) by A1, A2;
then A4: the_arity_of o1 = the_arity_of o2 by Th6;
o1 ~= o2 by A1;
hence o1 = o2 by A4, A3, Def3; :: thesis: verum