let A be preIfWhileAlgebra; :: thesis: EmptyIns A nin ElementaryInstructions A
set I = EmptyIns A;
EmptyIns A in {(EmptyIns A)} by TARSKI:def 1;
then EmptyIns A nin the carrier of A \ {(EmptyIns A)} by XBOOLE_0:def 5;
then EmptyIns A nin ( the carrier of A \ {(EmptyIns A)}) \ (rng (Den ((In (3,(dom the charact of A))),A))) by XBOOLE_0:def 5;
then EmptyIns A nin (( the carrier of A \ {(EmptyIns A)}) \ (rng (Den ((In (3,(dom the charact of A))),A)))) \ (rng (Den ((In (4,(dom the charact of A))),A))) by XBOOLE_0:def 5;
hence EmptyIns A nin ElementaryInstructions A by XBOOLE_0:def 5; :: thesis: verum