:: deftheorem defines <= MSUHOM_1:def 1 :
for S, S9 being non empty ManySortedSign holds
( S <= S9 iff ( the carrier of S c= the carrier of S9 & the carrier' of S c= the carrier' of S9 & the Arity of S9 | the carrier' of S = the Arity of S & the ResultSort of S9 | the carrier' of S = the ResultSort of S ) );