reconsider I = {[0,{},{}]} as non empty set ;
reconsider i = [0,{},{}] as Element of I by TARSKI:def 1;
take S = COM-Struct(# I,i #); :: thesis: ( the Instructions of S = {[0,{},{}]} & the haltF of S = [0,{},{}] )
thus ( the Instructions of S = {[0,{},{}]} & the haltF of S = [0,{},{}] ) ; :: thesis: verum