let R be Relation; :: thesis: for a, b being set st a,b are_critical_wrt R holds
a,b are_convertible_wrt R
let a, b be set ; :: thesis: ( a,b are_critical_wrt R implies a,b are_convertible_wrt R )
assume that
A1: a,b are_divergent<=1_wrt R and
not a,b are_convergent_wrt R ; :: according to REWRITE1:def 27 :: thesis: a,b are_convertible_wrt R
thus a,b are_convertible_wrt R by A1, Th38, Th46; :: thesis: verum