let R be Relation; :: thesis: for a, b being set holds
( R reduces a,b iff ( a = b or [a,b] in R [*] ) )
let a, b be set ; :: thesis: ( R reduces a,b iff ( a = b or [a,b] in R [*] ) )

hereby :: thesis: ( ( a = b or [a,b] in R [*] ) implies R reduces a,b )

assume A1: R reduces a,b ; :: thesis: ( a <> b implies [a,b] in R [*] )
then consider p being RedSequence of R such that
A2: ( a = p . 1 & b = p . (len p) ) by Def3;
assume a <> b ; :: thesis: [a,b] in R [*]
then A3: ( a in field R & b in field R ) by A1, Th19;
A4: len p >= 0 + 1 by NAT_1:13;

now

let i be Nat; :: thesis: ( i >= 1 & i < len p implies [(p . i),(p . (i + 1))] in R )
assume ( i >= 1 & i < len p ) ; :: thesis: [(p . i),(p . (i + 1))] in R
then ( i in dom p & i + 1 in dom p ) by Lm3, Lm4;
hence [(p . i),(p . (i + 1))] in R by Def2; :: thesis: verum

end;

hence [a,b] in R [*] by A2, A3, A4, FINSEQ_1:def 16; :: thesis: verum

end;

assume A5: ( ( a = b or [a,b] in R [*] ) & not R reduces a,b ) ; :: thesis: contradiction
then consider p being FinSequence such that
A6: ( len p >= 1 & p . 1 = a & p . (len p) = b ) and
A7: for i being Nat st i >= 1 & i < len p holds
[(p . i),(p . (i + 1))] in R by Th13, FINSEQ_1:def 16;
p is RedSequence of R

proof

thus len p > 0 by A6; :: according to REWRITE1:def 2 :: thesis: for i being Element of NAT st i in dom p & i + 1 in dom p holds
[(p . i),(p . (i + 1))] in R
let i be Element of NAT ; :: thesis: ( i in dom p & i + 1 in dom p implies [(p . i),(p . (i + 1))] in R )
assume ( i in dom p & i + 1 in dom p ) ; :: thesis: [(p . i),(p . (i + 1))] in R
then ( i >= 1 & i < len p ) by Lm1, Lm2;
hence [(p . i),(p . (i + 1))] in R by A7; :: thesis: verum

end;

hence contradiction by A5, A6, Def3; :: thesis: verum