:: deftheorem defines if-then-else AOFA_000:def 18 :
for A being non-empty with_if-instruction UAStr
for C, I1, I2 being Algorithm of A holds if-then-else (C,I1,I2) = (Den ((In (3,(dom the charact of A))),A)) . <*C,I1,I2*>;