let R be Relation; :: thesis: for a being set holds
( a,a are_convergent_wrt R & a,a are_divergent_wrt R )
let a be set ; :: thesis: ( a,a are_convergent_wrt R & a,a are_divergent_wrt R )
thus ( ex b being set st
( R reduces a,b & R reduces a,b ) & ex b being set st
( R reduces b,a & R reduces b,a ) ) by Th13; :: according to REWRITE1:def 7,REWRITE1:def 8 :: thesis: verum