:: deftheorem Def25 defines well_founded AOFA_000:def 25 :
for A being preIfWhileAlgebra holds
( A is well_founded iff ElementaryInstructions A is GeneratorSet of A );