[ngrilly]

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.