let S be OrderSortedSign; :: thesis: for o1, o2 being OperSymbol of S st S is monotone & the_arity_of o1 = {} & o1 ~= o2 & the_arity_of o2 = {} holds
o1 = o2
let o1, o2 be OperSymbol of S; :: thesis: ( S is monotone & the_arity_of o1 = {} & o1 ~= o2 & the_arity_of o2 = {} implies o1 = o2 )
assume that
A1: S is monotone and
A2: ( the_arity_of o1 = {} & o1 ~= o2 & the_arity_of o2 = {} ) ; :: 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, Def7;
then the_result_sort_of o1 = the_result_sort_of o2 by ORDERS_2:2;
hence o1 = o2 by A2, Def3; :: thesis: verum