let nt be NonTerminal of SCM-AE; :: thesis: not not nt = [0,0] & ... & not nt = [0,4]
consider x, y being object such that
A1: x in 1 and
A2: y in 5 and
A3: nt = [x,y] by Lm3, ZFMISC_1:84;
A4: x = 0 by A1, CARD_1:49, TARSKI:def 1;
consider n being Nat such that
A5: y = n and
A6: n < 5 by A2, Lm2;
5 = 4 + 1 ;
then n <= 4 by A6, NAT_1:13;
then not not n = 0 & ... & not n = 4 ;
hence not not nt = [0,0] & ... & not nt = [0,4] by A3, A4, A5; :: thesis: verum