Formalization and Models for the alternative Set Theory