let X be ARS ; :: thesis: ( not X is empty & the reduction of X is strongly-normalizing implies X is SN )
set R = the reduction of X;
set A = the carrier of X;
assume A1: not X is empty ; :: thesis: ( not the reduction of X is strongly-normalizing or X is SN )
assume A5: for f being ManySortedSet of NAT holds
not for i being Nat holds [(f . i),(f . (i + 1))] in the reduction of X ; :: according to REWRITE1:def 15 :: thesis: X is SN
let f be Function of NAT, the carrier of X; :: according to ABSRED_0:def 15 :: thesis: not for i being Nat holds f . i ==> f . (i + 1)
consider i being Nat such that
A6: not [(f . i),(f . (i + 1))] in the reduction of X by A1, A5;
take i ; :: thesis: not f . i ==> f . (i + 1)
thus not [(f . i),(f . (i + 1))] in the reduction of X by A6; :: according to ABSRED_0:def 1 :: thesis: verum