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

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