let R be Relation; :: thesis: for a, b being object st a,b are_convergent<=1_wrt R holds
a,b are_convergent_wrt R
let a, b be object ; :: thesis: ( a,b are_convergent<=1_wrt R implies a,b are_convergent_wrt R )
given c being object such that A1: ( ( [a,c] in R or a = c ) & ( [b,c] in R or b = c ) ) ; :: according to REWRITE1:def 9 :: thesis: a,b are_convergent_wrt R
take c ; :: according to REWRITE1:def 7 :: thesis: ( R reduces a,c & R reduces b,c )
thus ( R reduces a,c & R reduces b,c ) by A1, Th12, Th15; :: thesis: verum