set X = { I where I is Instruction of S : I is halting } ;
consider I being Instruction of S such that
A1: I is halting by Def9;
I in { I where I is Instruction of S : I is halting } by A1;
then choose { I where I is Instruction of S : I is halting } in { I where I is Instruction of S : I is halting } ;
then ex I being Instruction of S st
( choose { I where I is Instruction of S : I is halting } = I & I is halting ) ;
hence choose { I where I is Instruction of S : I is halting } is Instruction of S ; :: thesis: verum