let R be Relation; ( R is strongly-normalizing implies R is weakly-normalizing )
assume A1:
R is strongly-normalizing
; R is weakly-normalizing
let a be object ; REWRITE1:def 14 ( a in field R implies a has_a_normal_form_wrt R )
assume A2:
a in field R
; 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
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
; REWRITE1:def 11 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 REWRITE1:def 5,
REWRITE1:def 6 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
;
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;
verum
end;
thus
R reduces a,x
by A6; verum