let R be Relation; :: thesis: for a, b being set st a is_a_normal_form_wrt R & R reduces a,b holds
a = b
let a, b be set ; :: thesis: ( a is_a_normal_form_wrt R & R reduces a,b implies a = b )
assume A1: for b being set holds not [a,b] in R ; :: according to REWRITE1:def 5 :: thesis: ( not R reduces a,b or a = b )
assume R reduces a,b ; :: thesis: a = b
then consider p being FinSequence such that
A2: len p > 0 and
A3: p . 1 = a and
A4: p . (len p) = b and
A5: for i being Element of NAT st i in dom p & i + 1 in dom p holds
[(p . i),(p . (i + 1))] in R by Th12;

A6: now

assume len p > 1 ; :: thesis: contradiction
then ( 1 in dom p & 1 + 1 in dom p ) by Lm3, Lm4;
then [a,(p . (1 + 1))] in R by A3, A5;
hence contradiction by A1; :: thesis: verum

end;

len p >= 0 + 1 by A2, NAT_1:13;
hence a = b by A3, A4, A6, XXREAL_0:1; :: thesis: verum