let A be preIfWhileAlgebra; :: thesis: for I1, I2 being Element of A st I1 <> I1 \; I2 & I2 <> I1 \; I2 holds
I1 \; I2 nin ElementaryInstructions A
let I1, I2 be Element of A; :: thesis: ( I1 <> I1 \; I2 & I2 <> I1 \; I2 implies I1 \; I2 nin ElementaryInstructions A )
assume that
A1: I1 <> I1 \; I2 and
A2: I2 <> I1 \; I2 ; :: thesis: I1 \; I2 nin ElementaryInstructions A
I1 \; I2 in { (J1 \; J2) where J1, J2 is Algorithm of A : ( J1 <> J1 \; J2 & J2 <> J1 \; J2 ) } by A1, A2;
hence I1 \; I2 nin ElementaryInstructions A by XBOOLE_0:def 5; :: thesis: verum