It isn't clear whether the theorem as stated in set.mm can be proved and if so whether the proof will be similar to the set.mm one. Current guess: yes and no respectively. The reason for being skeptical this will be proved the same way is the use of things like set difference in the statement of restntr and excluded middle, e.g. df-or, in its proof.