 And then any such formula_10 is itself a member of an even larger “almost universal set” and so on.It's one of the strong cardinality axioms guaranteeing vastly more sets than one normally assumes to exist.The Mizar language, underlying the implementation of TG and providing its logical syntax, is typed and the types are assumed to be non-empty.