for A being preIfWhileAlgebra st A is free holds
for C, I1, I2 being Element of A holds
( EmptyIns A <> I1 \; I2 & EmptyIns A <> if-then-else (C,I1,I2) & EmptyIns A <> while (C,I1) )