for S being OrderSortedSign
for o1, o2 being OperSymbol of S
for A being OSAlgebra of S st o1 <= o2 holds
( Args (o1,A) c= Args (o2,A) & Result (o1,A) c= Result (o2,A) ) by Th24, Th25;