let R be Relation; 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 ; ( 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)
; REWRITE1:def 3 ( not a <> b or ( a in field R & b in field R ) )
A3:
len p >= 0 + 1
by NAT_1:13;
assume
a <> b
; ( 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; 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;
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; verum