let R be Relation; :: thesis: for a, b being object st R reduces a,b & not a in field R holds
a = b
let a, b be object ; :: thesis: ( R reduces a,b & not a in field R implies a = b )
given p being RedSequence of R such that A1: p . 1 = a and
A2: p . (len p) = b ; :: according to REWRITE1:def 3 :: thesis: ( a in field R or a = b )
assume A3: not a in field R ; :: thesis: a = b

A4: now :: thesis: not len p > 1

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

end;

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