let R be with_UN_property Relation; :: thesis: for a, b, c being set st b is_a_normal_form_of a,R & c is_a_normal_form_of a,R holds
b = c
let a, b, c be set ; :: thesis: ( b is_a_normal_form_of a,R & c is_a_normal_form_of a,R implies b = c )
assume that
A1: ( b is_a_normal_form_wrt R & R reduces a,b ) and
A2: ( c is_a_normal_form_wrt R & R reduces a,c ) ; :: according to REWRITE1:def 6 :: thesis: b = c
b,c are_divergent_wrt R by A1, A2, Def8;
then b,c are_convertible_wrt R by Th38;
hence b = c by A1, A2, Def19; :: thesis: verum