Theory exploration is a term describing the development of a formal (i.e. with the help of an automated proof-assistant) approach to selected topic, usually within mathematics or computer science. This activity however usually doesn't reflect the view of science considered as a whole, not as separated islands of knowledge. Merging theories essentially has its primary aim of bridging these gaps between specific disciplines. As the authors provided formal apparatus for basic notions within rough set theory (as e.g. approximation operators and membership functions), they try to reuse the knowledge which is already contained in available repositories of computer-checked mathematical knowledge, or which can be obtained in a relatively easy way.