theorem :: OSALG_1:10

for S being OrderSortedSign
for o1, o2 being OperSymbol of S st S is monotone & the_arity_of o1 = {} & o1 ~= o2 & the_arity_of o2 = {} holds
o1 = o2