let R be Relation; :: thesis: for a, b being object holds
( R reduces a,b iff ( a = b or [a,b] in R [*] ) )
let a, b be object ; :: 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) ) ;

A3: now :: thesis: for i being Nat st i >= 1 & i < len p holds
[(p . i),(p . (i + 1))] in R

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;

assume a <> b ; :: thesis: [a,b] in R [*]
then A4: ( a in field R & b in field R ) by A1, Th18;
len p >= 0 + 1 by NAT_1:13;
hence [a,b] in R [*] by A2, A4, A3, FINSEQ_1:def 17; :: thesis: verum

end;

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

proof

thus len p > 0 by A7; :: according to REWRITE1:def 2 :: thesis: for i being Nat st i in dom p & i + 1 in dom p holds
[(p . i),(p . (i + 1))] in R
let i be Nat; :: thesis: ( i in dom p & i + 1 in dom p implies [(p . i),(p . (i + 1))] in R )
assume that
A10: i in dom p and
A11: i + 1 in dom p ; :: thesis: [(p . i),(p . (i + 1))] in R
i >= 1 by A10, Lm1;
hence [(p . i),(p . (i + 1))] in R by A9, A11, Lm2; :: thesis: verum

end;

hence contradiction by A6, A8; :: thesis: verum