let R be Relation; :: thesis: for a, b being object holds
( R reduces a,b iff ex p being FinSequence st
( len p > 0 & p . 1 = a & p . (len p) = b & ( for i being Nat st i in dom p & i + 1 in dom p holds
[(p . i),(p . (i + 1))] in R ) ) )
let a, b be object ; :: thesis: ( R reduces a,b iff ex p being FinSequence st
( len p > 0 & p . 1 = a & p . (len p) = b & ( for i being Nat st i in dom p & i + 1 in dom p holds
[(p . i),(p . (i + 1))] in R ) ) )
thus ( R reduces a,b implies ex p being FinSequence st
( len p > 0 & p . 1 = a & p . (len p) = b & ( for i being Nat st i in dom p & i + 1 in dom p holds
[(p . i),(p . (i + 1))] in R ) ) ) :: thesis: ( ex p being FinSequence st
( len p > 0 & p . 1 = a & p . (len p) = b & ( for i being Nat st i in dom p & i + 1 in dom p holds
[(p . i),(p . (i + 1))] in R ) ) implies R reduces a,b )

proof

given p being RedSequence of R such that A1: ( p . 1 = a & p . (len p) = b ) ; :: according to REWRITE1:def 3 :: thesis: ex p being FinSequence st
( len p > 0 & p . 1 = a & p . (len p) = b & ( for i being Nat st i in dom p & i + 1 in dom p holds
[(p . i),(p . (i + 1))] in R ) )
take p ; :: thesis: ( len p > 0 & p . 1 = a & p . (len p) = b & ( for i being Nat st i in dom p & i + 1 in dom p holds
[(p . i),(p . (i + 1))] in R ) )
thus ( len p > 0 & p . 1 = a & p . (len p) = b & ( for i being Nat st i in dom p & i + 1 in dom p holds
[(p . i),(p . (i + 1))] in R ) ) by A1, Def2; :: thesis: verum

end;

given p being FinSequence such that A2: len p > 0 and
A3: ( p . 1 = a & p . (len p) = b ) and
A4: for i being Nat st i in dom p & i + 1 in dom p holds
[(p . i),(p . (i + 1))] in R ; :: thesis: R reduces a,b
reconsider p = p as RedSequence of R by A2, A4, Def2;
take p ; :: according to REWRITE1:def 3 :: thesis: ( p . 1 = a & p . (len p) = b )
thus ( p . 1 = a & p . (len p) = b ) by A3; :: thesis: verum