:: deftheorem defines for-do AOFA_000:def 21 :
for A being preIfWhileAlgebra
for I0, C, I, J being Element of A holds for-do (I0,C,J,I) = I0 \; (while (C,(I \; J)));