let R be Relation; 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 ; ( 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 )
; REWRITE1:def 3 ( a,b are_convertible_wrt R & b,a are_convertible_wrt R )
p is RedSequence of R \/ (R ~)
then
R \/ (R ~) reduces a,b
by A1;
hence
a,b are_convertible_wrt R
; b,a are_convertible_wrt R
hence
b,a are_convertible_wrt R
by Lm5; verum