theorem Th24: :: OSALG_1:24

for S being OrderSortedSign
for o1, o2 being OperSymbol of S
for A being OSAlgebra of S st the_result_sort_of o1 <= the_result_sort_of o2 holds
Result (o1,A) c= Result (o2,A)