theorem Th73: :: AOFA_000:73

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