theorem Th25: :: OSALG_1:25

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