let S be OrderSortedSign; :: thesis: 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) )
let o1, o2 be OperSymbol of S; :: thesis: for A being OSAlgebra of S st o1 <= o2 holds
( Args (o1,A) c= Args (o2,A) & Result (o1,A) c= Result (o2,A) )
let A be OSAlgebra of S; :: thesis: ( o1 <= o2 implies ( Args (o1,A) c= Args (o2,A) & Result (o1,A) c= Result (o2,A) ) )
assume o1 <= o2 ; :: thesis: ( Args (o1,A) c= Args (o2,A) & Result (o1,A) c= Result (o2,A) )
then ( the_arity_of o1 <= the_arity_of o2 & the_result_sort_of o1 <= the_result_sort_of o2 ) by Def22;
hence ( Args (o1,A) c= Args (o2,A) & Result (o1,A) c= Result (o2,A) ) by Th24, Th25; :: thesis: verum