:: deftheorem Def23 defines infinite AOFA_000:def 23 :
for A being preIfWhileAlgebra holds
( A is infinite iff ElementaryInstructions A is infinite );