theorem :: OSALG_1:22

for S being OrderSortedSign
for o1, o2 being OperSymbol of S st o1 <= o2 & o2 <= o1 holds
o1 = o2