let R be Relation; for a, b being object st a,b are_convertible_wrt R holds
b,a are_convertible_wrt R
let a, b be object ; ( a,b are_convertible_wrt R implies b,a are_convertible_wrt R )
assume
R \/ (R ~) reduces a,b
; REWRITE1:def 4 b,a are_convertible_wrt R
then
(R \/ (R ~)) ~ reduces b,a
by Th24;
then
(R ~) \/ ((R ~) ~) reduces b,a
by RELAT_1:23;
hence
R \/ (R ~) reduces b,a
; REWRITE1:def 4 verum