theorem Th89: :: AOFA_000:89

for A being free preIfWhileAlgebra
for C, I1, I2 being Element of A
for n being Nat st if-then-else (C,I1,I2) in (ElementaryInstructions A) |^ n holds
ex i being Nat st
( n = i + 1 & C in (ElementaryInstructions A) |^ i & I1 in (ElementaryInstructions A) |^ i & I2 in (ElementaryInstructions A) |^ i )