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 S₁[ 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 . (b₁ + 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 . (b₁ + 1) in field R
A8: i < len p by A7, Lm2;

per cases ( i = 0 or i > 0 ) ;

suppose i = 0 ; :: thesis: p . (b₁ + 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 . (b₁ + 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 S₁[k] holds
S₁[k + 1] ;
A10: S₁[ 0 ] by Lm1;
for i being Nat holds S₁[i] from NAT_1:sch 2(A10, A9);
hence b in field R by A2, A6; :: thesis: verum