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:103;
A4: x = 0 by A1, CARD_1:87, 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:29; :: thesis: verum