:: deftheorem defines if-then AOFA_000:def 19 :
for A being non-empty with_empty-instruction with_if-instruction UAStr
for C, I being Algorithm of A holds if-then (C,I) = if-then-else (C,I,(EmptyIns A));