theorem ex2eq (_R1 _R2: set): $ _R1 == _R2 -> ex2 _R1 == ex2 _R2 $;
_R1 == _R2 -> _R1 == _R2
_R1 == _R2 -> ex2 _R1 == ex2 _R2