let nt be NonTerminal of SCM-AE; :: thesis: ( nt = [0,0] or nt = [0,1] or nt = [0,2] or nt = [0,3] or nt = [0,4] )
consider x, y being set 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 Element of NAT such that
A5: y = n and
A6: n < 5 by A2, Lm2;
5 = 4 + 1 ;
then n <= 4 by A6, NAT_1:13;
hence ( nt = [0,0] or nt = [0,1] or nt = [0,2] or nt = [0,3] or nt = [0,4] ) by A3, A4, A5, NAT_1:28; :: thesis: verum