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