:: deftheorem Def16 defines terminating MSAFREE4:def 16 :
for I being set
for X being ManySortedSet of I
for R being ManySortedRelation of X holds
( R is terminating iff for x being set st x in I holds
R . x is strongly-normalizing );