"There is a finite set G such that for all standard f." For any set S, the intersection of S with the set G is a finite subset of S that contains every standard element of S. G is necessarily nonstandard. S: Standardisation If is any formula (it may be external) without a free occurrence of y, the universal closure of is an axiom. In words: If A is a standard set and P any property, internal or otherwise, then there is a unique, standard subset B of A whose standard elements are precisely the standard elements of A satisfying P (but the behaviour of B's nonstandard elements is not prescribed). T: Transfer If is an internal formula with no other free variables than those indicated, then is an axiom. In words: If all the parameters A, B, C, ..., W of an internal formula F have standard values then holds for all xs as soon as it holds for all standard xs—from which it follows that all uniquely defined concepts or objects within classical mathematics are standard. Formal justification for the axioms Aside from the intuitive motivations suggested above, it is necessary to justify that additional IST axioms do not lead to errors or inconsistencies in reasoning. Mistakes and philosophical weaknesses in reasoning about infinitesimal numbers in the work of Gottfried Leibniz, Johann Bernoulli, Leonhard Euler, Augustin-Louis Cauchy, and others were the reason that they were originally abandoned for the more cumbersome real number-based arguments developed by Georg Cantor, Richard Dedekind, and Karl Weierstrass, which were perceived as being more rigorous by Weierstrass's followers. The approach for internal set theory is the same as that for any new axiomatic system—we construct a model for the new axioms using the elements of a simpler, more trusted, axiom scheme. This is quite similar to justifying the consistency of the axioms of elliptic non-Euclidean geometry by noting they can be modeled by an appropriate interpretation of great circles on a sphere in ordinary 3-space. In fact via a suitable model a proof can be given of the relative consistency of IST as compared with ZFC: if ZFC is consistent, then IST is consistent. In fact, a stronger statement can be made: IST is a conservative extension of ZFC: any internal formula that can be proven within internal set theory can be proven in the Zermelo–Fraenkel axioms with the axiom of choice alone.