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 & y in 5 & nt = [x,y] ) by Lm3, ZFMISC_1:103;
A2: x = 0 by A1, CARD_1:87, TARSKI:def 1;
consider n being Element of NAT such that
A3: ( y = n & n < 5 ) by A1, Lm2;
5 = 4 + 1 ;
then n <= 4 by A3, NAT_1:13;
hence ( nt = [0 ,0 ] or nt = [0 ,1] or nt = [0 ,2] or nt = [0 ,3] or nt = [0 ,4] ) by A1, A2, A3, NAT_1:29; :: thesis: verum