2 ms·

Thanks a lot @lmm. Now I get it :) About Mizar, I don't know if you can use it without the additional axioms of Tarski-Grothendieck set theory.