A1: [0,0,0] <> [1,0,0] by XTUPLE_0:3;
the InstructionsF of (STC N) = {[0,0,0],[1,0,0]} by AMISTD_1:def 7;
then ( [0,0,0] in the InstructionsF of (STC N) & [1,0,0] in the InstructionsF of (STC N) ) by TARSKI:def 2;
hence not the InstructionsF of (STC N) is trivial by A1, ZFMISC_1:def 10; :: according to AMISTD_4:def 1 :: thesis: verum