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