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; AMISTD_4:def 1 verum