let R be Relation; :: thesis: for a, b being object st R reduces a,b holds
( a,b are_convertible_wrt R & b,a are_convertible_wrt R )
let a, b be object ; :: 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 Nat st i in dom p & i + 1 in dom p holds
[(p . i),(p . (i + 1))] in R \/ (R ~)
let i be 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;
hence a,b are_convertible_wrt R ; :: thesis: b,a are_convertible_wrt R
hence b,a are_convertible_wrt R by Lm5; :: thesis: verum