let R be Relation; :: thesis: for a, b being set st a,b are_convertible_wrt R holds
b,a are_convertible_wrt R
let a, b be set ; :: 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 Th25;
then (R ~ ) \/ ((R ~ ) ~ ) reduces b,a by RELAT_1:40;
hence R \/ (R ~ ) reduces b,a ; :: according to REWRITE1:def 4 :: thesis: verum