let N be non empty with_non-empty_elements set ; :: thesis: for i being Element of the Instructions of (STC N) holds
( InsCode i = 1 or InsCode i = 0 )
let i be Element of the Instructions of (STC N); :: thesis: ( InsCode i = 1 or InsCode i = 0 )
the Instructions of (STC N) = {[1,0 ,0 ],[0 ,0 ,0 ]} by Def11;
then ( i = [1,0 ,0 ] or i = [0 ,0 ,0 ] ) by TARSKI:def 2;
hence ( InsCode i = 1 or InsCode i = 0 ) by RECDEF_2:def 1; :: thesis: verum