let R be Relation; 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 ; ( 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
; REWRITE1:def 5 ( not R reduces a,b or a = b )
assume
R reduces a,b
; 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; verum