:: deftheorem defines strongly-normalizing REWRITE1:def 15 :
for R being Relation holds
( R is strongly-normalizing iff for f being ManySortedSet of NAT holds
not for i being Nat holds [(f . i),(f . (i + 1))] in R );