defpred S1[ object ] means verum;
let R be Relation; ( R is strongly-normalizing implies ( R is irreflexive & R is co-well_founded ) )
assume A1:
for f being ManySortedSet of NAT holds
not for i being Nat holds [(f . i),(f . (i + 1))] in R
; REWRITE1:def 15 ( R is irreflexive & R is co-well_founded )
thus
R is irreflexive
R is co-well_founded
defpred S2[ object , object ] means [c1,c2] in R;
let Y be set ; REWRITE1:def 16 ( Y c= field R & Y <> {} implies ex a being object st
( a in Y & ( for b being object st b in Y & a <> b holds
not [a,b] in R ) ) )
assume that
Y c= field R
and
A4:
Y <> {}
and
A5:
for a being object st a in Y holds
ex b being object st
( b in Y & a <> b & [a,b] in R )
; contradiction
reconsider Y = Y as non empty set by A4;
then A6:
for x being object st x in Y & S1[x] holds
ex y being object st
( y in Y & S2[x,y] & S1[y] )
;
set y = the Element of Y;
A7:
( the Element of Y in Y & S1[ the Element of Y] )
;
consider f being Function such that
A8:
( dom f = NAT & rng f c= Y & f . 0 = the Element of Y )
and
A9:
for k being Nat holds
( S2[f . k,f . (k + 1)] & S1[f . k] )
from TREES_2:sch 5(A7, A6);
f is ManySortedSet of NAT
by A8, PARTFUN1:def 2, RELAT_1:def 18;
hence
contradiction
by A1, A9; verum