for A being preIfWhileAlgebra st A is free holds
for C, I, D, J being Element of A holds
( while (C,I) <> C & while (C,I) <> I & ( while (C,I) = while (D,J) implies ( C = D & I = J ) ) )