let R be Relation; :: thesis: for a, b being object st R reduces a,b & a <> b holds
( a in field R & b in field R )
let a, b be object ; :: thesis: ( R reduces a,b & a <> b implies ( a in field R & b in field R ) )
given p being RedSequence of R such that A1: a = p . 1 and
A2: b = p . (len p) ; :: according to REWRITE1:def 3 :: thesis: ( not a <> b or ( a in field R & b in field R ) )
A3: len p >= 0 + 1 by NAT_1:13;
assume a <> b ; :: thesis: ( a in field R & b in field R )
then len p > 1 by A1, A2, A3, XXREAL_0:1;
then A4: 1 + 1 in dom p by Lm4;
1 in dom p by A3, Lm3;
then A5: [a,(p . 2)] in R by A1, A4, Def2;
hence a in field R by RELAT_1:15; :: thesis: b in field R
defpred S1[ Nat] means ( $1 in dom p implies p . $1 in field R );
A6: len p in dom p by FINSEQ_5:6;
now :: thesis: for i being Nat st ( i in dom p implies p . i in field R ) & i + 1 in dom p holds
p . (i + 1) in field R
let i be Nat; :: thesis: ( ( i in dom p implies p . i in field R ) & i + 1 in dom p implies p . (b1 + 1) in field R )
assume that
( i in dom p implies p . i in field R ) and
A7: i + 1 in dom p ; :: thesis: p . (b1 + 1) in field R
A8: i < len p by A7, Lm2;
per cases ( i = 0 or i > 0 ) ;
suppose i = 0 ; :: thesis: p . (b1 + 1) in field R
hence p . (i + 1) in field R by A1, A5, RELAT_1:15; :: thesis: verum
end;
suppose i > 0 ; :: thesis: p . (b1 + 1) in field R
then i in dom p by A8, Lm3;
then [(p . i),(p . (i + 1))] in R by A7, Def2;
hence p . (i + 1) in field R by RELAT_1:15; :: thesis: verum
end;
end;
end;
then A9: for k being Nat st S1[k] holds
S1[k + 1] ;
A10: S1[ 0 ] by Lm1;
for i being Nat holds S1[i] from NAT_1:sch 2(A10, A9);
 hence b in field R by A2, A6; :: thesis: verum