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 object ; :: 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 object ; :: 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 by Th12;
then a in { x where x is Element of X : R reduces a,x } by A2;
then consider x being object such that
A4: x in { x where x is Element of X : R reduces a,x } and
A5: for b being object st b in { x where x is Element of X : R reduces a,x } & x <> b holds
not [x,b] in R by A1, 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 A4;

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

R is_irreflexive_in field R by A1, RELAT_2:def 10;
then A7: not [x,x] in R by A3, A4;
given b being object such that A8: [x,b] in R ; :: thesis: contradiction
R reduces x,b by A8, Th15;
then A9: R reduces a,b by A6, Th16;
b in X by A8, RELAT_1:15;
then b in { x where x is Element of X : R reduces a,x } by A9;
hence contradiction by A5, A8, A7; :: thesis: verum

end;

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