let R be Relation; :: thesis: for a, b being set st a,b are_divergent_wrt R holds
b,a are_divergent_wrt R
let a, b be set ; :: thesis: ( a,b are_divergent_wrt R implies b,a are_divergent_wrt R )
assume ex c being set st
( R reduces c,a & R reduces c,b ) ; :: according to REWRITE1:def 8 :: thesis: b,a are_divergent_wrt R
hence ex c being set st
( R reduces c,b & R reduces c,a ) ; :: according to REWRITE1:def 8 :: thesis: verum