let A be preIfWhileAlgebra; ( A is well_founded iff for I being Element of A ex n being Nat st I in (ElementaryInstructions A) |^ n )
set B = ElementaryInstructions A;
( A is well_founded iff ElementaryInstructions A is GeneratorSet of A )
by Def25;
hence
( A is well_founded iff for I being Element of A ex n being Nat st I in (ElementaryInstructions A) |^ n )
by Th30; verum