theorem Th1: :: SCM_COMP:1
for nt being NonTerminal of SCM-AE holds
not not nt = [0,0] & ... & not nt = [0,4]