let R be Relation; :: thesis: for a, b being object st a is_a_normal_form_wrt R & R reduces a,b holds
a = b
let a, b be object ; :: thesis: ( a is_a_normal_form_wrt R & R reduces a,b implies a = b )
assume A1: for b being object 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 Nat st i in dom p & i + 1 in dom p holds
[(p . i),(p . (i + 1))] in R by Th11;
len p >= 0 + 1 by A2, NAT_1:13;
hence a = b by A3, A4, A6, XXREAL_0:1; :: thesis: verum