let R be Relation; :: thesis: ( R is co-well_founded & R is irreflexive implies R is strongly-normalizing )
assume A10: for Y being set st Y c= field R & Y <> {} holds
ex a being set st
( a in Y & ( for b being set st b in Y & a <> b holds
not [a,b] in R ) ) ; :: according to REWRITE1:def 16 :: thesis: ( not R is irreflexive or R is strongly-normalizing )
assume A11: for x being set st x in field R holds
not [x,x] in R ; :: according to RELAT_2:def 2,RELAT_2:def 10 :: thesis: R is strongly-normalizing
let f be ManySortedSet of NAT ; :: according to REWRITE1:def 15 :: thesis: not for i being Element of NAT holds [(f . i),(f . (i + 1))] in R
assume A12: for i being Element of NAT holds [(f . i),(f . (i + 1))] in R ; :: thesis: contradiction
A13: dom f = NAT by PBOOLE:def 3;
A14: rng f c= field R

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in rng f or y in field R )
assume y in rng f ; :: thesis: y in field R
then consider x being set such that
A15: ( x in dom f & y = f . x ) by FUNCT_1:def 5;
reconsider x = x as Element of NAT by A15, PBOOLE:def 3;
[y,(f . (x + 1))] in R by A12, A15;
hence y in field R by RELAT_1:30; :: thesis: verum

end;

f . 0 in rng f by A13, FUNCT_1:def 5;
then consider a being set such that
A16: ( a in rng f & ( for b being set st b in rng f & a <> b holds
not [a,b] in R ) ) by A10, A14;
consider x being set such that
A17: ( x in dom f & a = f . x ) by A16, FUNCT_1:def 5;
reconsider x = x as Element of NAT by A17, PBOOLE:def 3;
A18: ( [a,(f . (x + 1))] in R & not [a,a] in R ) by A11, A12, A14, A16, A17;
then ( a <> f . (x + 1) & f . (x + 1) in rng f ) by A13, FUNCT_1:def 5;
hence contradiction by A16, A18; :: thesis: verum