let R be Relation; :: thesis: ( R is with_NF_property implies R is with_UN_property )
assume A15: for a, b being set st a is_a_normal_form_wrt R & a,b are_convertible_wrt R holds
R reduces b,a ; :: according to REWRITE1:def 20 :: thesis: R is with_UN_property
let a, b be set ; :: according to REWRITE1:def 19 :: thesis: ( a is_a_normal_form_wrt R & b is_a_normal_form_wrt R & a,b are_convertible_wrt R implies a = b )
assume ( a is_a_normal_form_wrt R & b is_a_normal_form_wrt R & a,b are_convertible_wrt R ) ; :: thesis: a = b
hence a = b by A15, Th34; :: thesis: verum