(idealisation principle cont.) I think that it's been applied wrongly here, though. There's no quantifier inversion in that axiom, you just eliminate the outer quantification over all finite sets of standard numbers from which the inner forall is sampled, then replace the inner forall with a forall-st. In this example, to turn the x and y standard, they would already need to be under the existential, and the lemma would have to be true taking x and y from all finite standard sets.

For the confused, the idealisation principle is an axiom of Internal Set Theory (i.e. an infinitesimal theory).