defpred S₁[ set ] 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 holds
not for i being Element of 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 set 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:19;
then reconsider f = NAT --> x as ManySortedSet of by PARTFUN1:def 4, RELAT_1:def 18;
consider i being Element of NAT such that
A3: not [(f . i),(f . (i + 1))] in R by A1;
f . i = x by FUNCOP_1:13;
hence contradiction by A2, A3, FUNCOP_1:13; :: thesis: verum

end;

defpred S₂[ set , set ] means [c₁,c₂] in R;
let Y be set ; :: according to REWRITE1:def 16 :: thesis: ( Y c= field R & Y <> {} implies ex a being set st
( a in Y & ( for b being set 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 set st a in Y holds
ex b being set st
( b in Y & a <> b & [a,b] in R ) ; :: thesis: contradiction
reconsider Y = Y as non empty set by A4;

now

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

end;

then A6: for x being set st x in Y & S₁[x] holds
ex y being set st
( y in Y & S₂[x,y] & S₁[y] ) ;
consider y being Element of Y;
A7: ( y in Y & S₁[y] ) ;
consider f being Function such that
A8: ( dom f = NAT & rng f c= Y & f . 0 = y ) and
A9: for k being Element of NAT holds
( S₂[f . k,f . (k + 1)] & S₁[f . k] ) from TREES_2:sch 5(A7, A6);
f is ManySortedSet of by A8, PARTFUN1:def 4, RELAT_1:def 18;
hence contradiction by A1, A9; :: thesis: verum