:: deftheorem defines tolerates CIRCCOMB:def 1 :
for S1, S2 being ManySortedSign holds
( S1 tolerates S2 iff ( the Arity of S1 tolerates the Arity of S2 & the ResultSort of S1 tolerates the ResultSort of S2 ) );