for A being preIfWhileAlgebra holds
( A is well_founded iff for I being Element of A ex n being Nat st I in (ElementaryInstructions A) |^ n ) by Th30;