connected set_relationTheory with relationTheory

Many definitions of set_relationTheory and relationTheory are
very similar and can be transformed into each other. The main difference
is that set_relationTheory uses set syntax, while relationTheory
predicate syntax. Moreover, set_relationTheory uses for some definitions
an explicitly restricted domain, while relationTheory operates on the
whole universe.

I added mappings between the definitions in set_relationTheory and
relationTheory. This allows to move between both worlds easily for
many definitions. Therefore, some proofs, especially when translating
from Lem into HOL and looking for well-founded relations become simpler.