ex Q being complete Relation st
( field Q c= field R & ( for a, b being object holds
( a,b are_convertible_wrt R iff a,b are_convergent_wrt Q ) ) ) by Th62;
hence ex b₁ being complete Relation st
for a, b being object holds
( a,b are_convertible_wrt R iff a,b are_convergent_wrt b₁ ) ; :: thesis: verum