take STC N ; :: thesis: ( STC N is with_explicit_jumps & STC N is IC-relocable & 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 7, MCART_1:25;
then not the Instructions of (STC N) is trivial by A1, ZFMISC_1:def 10;
hence ( STC N is with_explicit_jumps & STC N is IC-relocable & STC N is with_non_trivial_ObjectKinds & STC N is with_non_trivial_Instructions ) by Def1; :: thesis: verum