take STC N ; :: thesis: ( STC N is with_explicit_jumps & STC N is IC-good & STC N is Exec-preserving & STC N is with_non_trivial_ObjectKinds & STC N is with_non_trivial_Instructions )
A1: ( [1,0,0] in {[1,0,0],[0,0,0]} & [0,0,0] in {[1,0,0],[0,0,0]} ) by TARSKI:def 2;
( the Instructions of (STC N) = {[0,0,0],[1,0,0]} & [1,0,0] <> [0,0,0] ) by AMISTD_1:def 11, MCART_1:28;
then not the Instructions of (STC N) is trivial by A1, YELLOW_8:def 1;
hence ( STC N is with_explicit_jumps & STC N is IC-good & STC N is Exec-preserving & STC N is with_non_trivial_ObjectKinds & STC N is with_non_trivial_Instructions ) by Def1; :: thesis: verum