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