let R be Relation; :: thesis: ( R is strongly-normalizing implies R is weakly-normalizing )
assume A1: R is strongly-normalizing ; :: thesis: R is weakly-normalizing
let a be set ; :: according to REWRITE1:def 14 :: thesis: ( a in field R implies a has_a_normal_form_wrt R )
assume A2: a in field R ; :: thesis: a has_a_normal_form_wrt R
then reconsider X = field R as non empty set ;
set Y = { x where x is Element of X : R reduces a,x } ;
A3: { x where x is Element of X : R reduces a,x } c= field R

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in { x where x is Element of X : R reduces a,x } or y in field R )
assume y in { x where x is Element of X : R reduces a,x } ; :: thesis: y in field R
then ex x being Element of X st
( y = x & R reduces a,x ) ;
hence y in field R ; :: thesis: verum

end;

( R reduces a,a & a in X ) by A2, Th13;
then A4: ( a in { x where x is Element of X : R reduces a,x } & R is strongly-normalizing Relation ) by A1;
then consider x being set such that
A5: ( x in { x where x is Element of X : R reduces a,x } & ( for b being set st b in { x where x is Element of X : R reduces a,x } & x <> b holds
not [x,b] in R ) ) by A3, Def16;
take x ; :: according to REWRITE1:def 11 :: thesis: x is_a_normal_form_of a,R
A6: ex y being Element of X st
( x = y & R reduces a,y ) by A5;

hereby :: according to REWRITE1:def 5,REWRITE1:def 6 :: thesis: R reduces a,x

given b being set such that A7: [x,b] in R ; :: thesis: contradiction
( x in field R & R is_irreflexive_in field R & R reduces x,b ) by A3, A4, A5, A7, Th16, RELAT_2:def 10;
then ( not [x,x] in R & R reduces a,b & b in X ) by A6, A7, Th17, RELAT_1:30, RELAT_2:def 2;
then ( x <> b & b in { x where x is Element of X : R reduces a,x } ) by A7;
hence contradiction by A5, A7; :: thesis: verum

end;

thus R reduces a,x by A6; :: thesis: verum