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 and
A2: R reduces a,b and
A3: c is_a_normal_form_wrt R and
A4: R reduces a,c ; :: according to REWRITE1:def 6 :: thesis: b = c
b,c are_divergent_wrt R by A2, A4, Def8;
then b,c are_convertible_wrt R by Th38;
hence b = c by A1, A3, Def19; :: thesis: verum