let R be Relation; :: thesis: ( R is empty implies ( R is weakly-normalizing & R is strongly-normalizing ) )
assume A1: R is empty ; :: thesis: ( R is weakly-normalizing & R is strongly-normalizing )
thus R is weakly-normalizing :: thesis: R is strongly-normalizing

proof

let x be set ; :: according to REWRITE1:def 14 :: thesis: ( x in field R implies x has_a_normal_form_wrt R )
thus ( x in field R implies x has_a_normal_form_wrt R ) by A1, RELAT_1:40; :: thesis: verum

end;

thus R is strongly-normalizing :: thesis: verum

proof

let f be ManySortedSet of NAT ; :: according to REWRITE1:def 15 :: thesis: not for i being Element of NAT holds [(f . i),(f . (i + 1))] in R
take 0 ; :: thesis: not [(f . 0),(f . (0 + 1))] in R
thus not [(f . 0),(f . (0 + 1))] in R by A1; :: thesis: verum

end;