let R be Relation; :: thesis: for a, b being set st R reduces a,b holds
( a,b are_convertible_wrt R & b,a are_convertible_wrt R )
let a, b be set ; :: thesis: ( R reduces a,b implies ( a,b are_convertible_wrt R & b,a are_convertible_wrt R ) )
given p being RedSequence of R such that A1: ( p . 1 = a & p . (len p) = b ) ; :: according to REWRITE1:def 3 :: thesis: ( a,b are_convertible_wrt R & b,a are_convertible_wrt R )
p is RedSequence of R \/ (R ~)

proof

thus len p > 0 ; :: 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 \/ (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 \/ (R ~) )
assume ( i in dom p & i + 1 in dom p ) ; :: thesis: [(p . i),(p . (i + 1))] in R \/ (R ~)
then [(p . i),(p . (i + 1))] in R by Def2;
hence [(p . i),(p . (i + 1))] in R \/ (R ~) by XBOOLE_0:def 3; :: thesis: verum

end;

then R \/ (R ~) reduces a,b by A1, Def3;
hence a,b are_convertible_wrt R by Def4; :: thesis: b,a are_convertible_wrt R
hence b,a are_convertible_wrt R by Lm5; :: thesis: verum