let R be Relation; :: thesis: for a, b being object st a,b are_convertible_wrt R holds
b,a are_convertible_wrt R
let a, b be object ; :: thesis: ( a,b are_convertible_wrt R implies b,a are_convertible_wrt R )
assume R \/ (R ~) reduces a,b ; :: according to REWRITE1:def 4 :: thesis: 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 ; :: according to REWRITE1:def 4 :: thesis: verum