theorem Th62: :: REWRITE1:62

for R being Relation 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 ) ) )