let R be Relation; :: thesis: for a, b being set st a,b are_divergent<=1_wrt R holds
a,b are_divergent_wrt R
let a, b be set ; :: thesis: ( a,b are_divergent<=1_wrt R implies a,b are_divergent_wrt R )
given c being set such that A1: ( ( [c,a] in R or a = c ) & ( [c,b] in R or b = c ) ) ; :: according to REWRITE1:def 10 :: thesis: a,b are_divergent_wrt R
take c ; :: according to REWRITE1:def 8 :: thesis: ( R reduces c,a & R reduces c,b )
thus ( R reduces c,a & R reduces c,b ) by A1, Th13, Th16; :: thesis: verum