defpred S₁[ object ] means verum;
let R be Relation; :: thesis: ( 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 ; :: according to REWRITE1:def 15 :: thesis: ( R is irreflexive & R is co-well_founded )
thus R is irreflexive :: thesis: R is co-well_founded

proof

given x being object such that x in field R and
A2: [x,x] in R ; :: according to RELAT_2:def 2,RELAT_2:def 10 :: thesis: contradiction
dom (NAT --> x) = NAT by FUNCOP_1:13;
then reconsider f = NAT --> x as ManySortedSet of NAT by PARTFUN1:def 2, RELAT_1:def 18;
consider i being Nat such that
A3: not [(f . i),(f . (i + 1))] in R by A1;
i in NAT by ORDINAL1:def 12;
then f . i = x by FUNCOP_1:7;
hence contradiction by A2, A3, FUNCOP_1:7; :: thesis: verum

end;

defpred S₂[ object , object ] means [c₁,c₂] in R;
let Y be set ; :: according to REWRITE1:def 16 :: thesis: ( 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 ) ; :: thesis: contradiction
reconsider Y = Y as non empty set by A4;

now :: thesis: for x being set st x in Y holds
ex y being object st
( y in Y & [x,y] in R )

let x be set ; :: thesis: ( x in Y implies ex y being object st
( y in Y & [x,y] in R ) )
assume x in Y ; :: thesis: ex y being object st
( y in Y & [x,y] in R )
then ex b being object st
( b in Y & x <> b & [x,b] in R ) by A5;
hence ex y being object st
( y in Y & [x,y] in R ) ; :: thesis: verum

end;

then A6: for x being object st x in Y & S₁[x] holds
ex y being object st
( y in Y & S₂[x,y] & S₁[y] ) ;
set y = the Element of Y;
A7: ( the Element of Y in Y & S₁[ 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
( S₂[f . k,f . (k + 1)] & S₁[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; :: thesis: verum