let A be preIfWhileAlgebra; :: thesis: ( A is free implies ( A is well_founded & not A is degenerated ) )
assume A1: A is free ; :: thesis: ( A is well_founded & not A is degenerated )
then reconsider A' = A as free Universal_Algebra ;
consider G being free GeneratorSet of A';
Generators A = G by Th34;
hence ElementaryInstructions A is GeneratorSet of A by Th31, Th71; :: according to AOFA_000:def 25 :: thesis: not A is degenerated
thus for I1, I2 being Element of A holds
( not ( I1 <> EmptyIns A & I1 \; I2 = I2 ) & not ( I2 <> EmptyIns A & I1 \; I2 = I1 ) & not ( ( I1 <> EmptyIns A or I2 <> EmptyIns A ) & I1 \; I2 = EmptyIns A ) ) by A1, Th72, Th73; :: according to AOFA_000:def 24 :: thesis: ( ( for C, I1, I2 being Element of A holds not if-then-else C,I1,I2 = EmptyIns A ) & ( for C, I being Element of A holds not while C,I = EmptyIns A ) & ( for I1, I2, C, J1, J2 being Element of A holds
( not I1 <> EmptyIns A or not I2 <> EmptyIns A or not I1 \; I2 = if-then-else C,J1,J2 ) ) & ( for I1, I2, C, J being Element of A holds
( not I1 <> EmptyIns A or not I2 <> EmptyIns A or not I1 \; I2 = while C,J ) ) & ( for C1, I1, I2, C2, J being Element of A holds not if-then-else C1,I1,I2 = while C2,J ) )
thus ( ( for C, I1, I2 being Element of A holds not if-then-else C,I1,I2 = EmptyIns A ) & ( for C, I being Element of A holds not while C,I = EmptyIns A ) & ( for I1, I2, C, J1, J2 being Element of A holds
( not I1 <> EmptyIns A or not I2 <> EmptyIns A or not I1 \; I2 = if-then-else C,J1,J2 ) ) & ( for I1, I2, C, J being Element of A holds
( not I1 <> EmptyIns A or not I2 <> EmptyIns A or not I1 \; I2 = while C,J ) ) & ( for C1, I1, I2, C2, J being Element of A holds not if-then-else C1,I1,I2 = while C2,J ) ) by A1, Th72, Th73, Th74; :: thesis: verum