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 object st
( a in Y & ( for b being object 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 object 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 Nat holds [(f . i),(f . (i + 1))] in R
assume A12: for i being Nat holds [(f . i),(f . (i + 1))] in R ; :: thesis: contradiction
A13: rng f c= field R
proof
let y be object ; :: 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 object such that
A14: x in dom f and
A15: y = f . x by FUNCT_1:def 3;
reconsider x = x as Element of NAT by A14, PARTFUN1:def 2;
[y,(f . (x + 1))] in R by A12, A15;
hence y in field R by RELAT_1:15; :: thesis: verum
end;
A16: dom f = NAT by PARTFUN1:def 2;
then f . 0 in rng f by FUNCT_1:def 3;
then consider a being object such that
A17: a in rng f and
A18: for b being object st b in rng f & a <> b holds
not [a,b] in R by A10, A13;
consider x being object such that
A19: x in dom f and
A20: a = f . x by A17, FUNCT_1:def 3;
reconsider x = x as Element of NAT by A19, PARTFUN1:def 2;
A21: f . (x + 1) in rng f by A16, FUNCT_1:def 3;
A22: [a,(f . (x + 1))] in R by A12, A20;
then a <> f . (x + 1) by A11, A13, A17;
hence contradiction by A18, A22, A21; :: thesis: verum