let A be preIfWhileAlgebra; :: thesis: Generators A c= ElementaryInstructions A
let x be set ; :: according to TARSKI:def 3 :: thesis: ( x nin Generators A or not x nin ElementaryInstructions A )
assume that
A1: x in Generators A and
A2: x nin ElementaryInstructions A ; :: thesis: contradiction
reconsider x = x as Element of A by A1;
dom (Den (In 1,(dom the charact of A)),A) = {{} } by Th42;
then A3: {} in dom (Den (In 1,(dom the charact of A)),A) by TARSKI:def 1;

per cases ( x = EmptyIns A or ex I1, I2 being Element of A st
( x = I1 \; I2 & I1 <> I1 \; I2 & I2 <> I1 \; I2 ) or ex C, I1, I2 being Element of A st x = if-then-else C,I1,I2 or ex C, J being Element of A st x = while C,J ) by A2, Th53;

suppose x = EmptyIns A ; :: thesis: contradiction

then x in rng (Den (In 1,(dom the charact of A)),A) by A3, FUNCT_1:12;
hence contradiction by A1, Th26; :: thesis: verum

end;

suppose ex I1, I2 being Element of A st
( x = I1 \; I2 & I1 <> I1 \; I2 & I2 <> I1 \; I2 ) ; :: thesis: contradiction

then consider I1, I2 being Element of A such that
A4: x = I1 \; I2 and
I1 <> I1 \; I2 and
I2 <> I1 \; I2 ;
dom (Den (In 2,(dom the charact of A)),A) = 2 -tuples_on the carrier of A by Th44;
then <*I1,I2*> in dom (Den (In 2,(dom the charact of A)),A) by FINSEQ_2:157;
then x in rng (Den (In 2,(dom the charact of A)),A) by A4, FUNCT_1:12;
hence contradiction by A1, Th26; :: thesis: verum

end;

suppose ex C, I1, I2 being Element of A st x = if-then-else C,I1,I2 ; :: thesis: contradiction

then consider C, I1, I2 being Element of A such that
A5: x = if-then-else C,I1,I2 ;
dom (Den (In 3,(dom the charact of A)),A) = 3 -tuples_on the carrier of A by Th47;
then <*C,I1,I2*> in dom (Den (In 3,(dom the charact of A)),A) by FINSEQ_2:159;
then x in rng (Den (In 3,(dom the charact of A)),A) by A5, FUNCT_1:12;
hence contradiction by A1, Th26; :: thesis: verum

end;

suppose ex C, J being Element of A st x = while C,J ; :: thesis: contradiction

then consider C, J being Element of A such that
A6: x = while C,J ;
dom (Den (In 4,(dom the charact of A)),A) = 2 -tuples_on the carrier of A by Th48;
then <*C,J*> in dom (Den (In 4,(dom the charact of A)),A) by FINSEQ_2:157;
then x in rng (Den (In 4,(dom the charact of A)),A) by A6, FUNCT_1:12;
hence contradiction by A1, Th26; :: thesis: verum

end;

end;