let R be Relation; :: thesis: ( R is with_Church-Rosser_property implies R is with_NF_property )
assume A13: R is with_Church-Rosser_property ; :: thesis: R is with_NF_property
let b, a be object ; :: according to REWRITE1:def 20 :: thesis: ( b is_a_normal_form_wrt R & b,a are_convertible_wrt R implies R reduces a,b )
assume A14: b is_a_normal_form_wrt R ; :: thesis: ( not b,a are_convertible_wrt R or R reduces a,b )
assume b,a are_convertible_wrt R ; :: thesis: R reduces a,b
then b,a are_convergent_wrt R by A13;
then ex c being object st
( R reduces b,c & R reduces a,c ) ;
hence R reduces a,b by A14, Th33; :: thesis: verum