:: deftheorem defines while AOFA_000:def 20 :
for A being non-empty with_while-instruction UAStr
for C, I being Algorithm of A holds while (C,I) = (Den ((In (4,(dom the charact of A))),A)) . <*C,I*>;