( 0 in 1 & 0 in 5 & 1 in 5 & 2 in 5 & 3 in 5 & 4 in 5 ) by Lm1, Lm2;
hence ( [0 ,0 ] is NonTerminal of SCM-AE & [0 ,1] is NonTerminal of SCM-AE & [0 ,2] is NonTerminal of SCM-AE & [0 ,3] is NonTerminal of SCM-AE & [0 ,4] is NonTerminal of SCM-AE ) by Lm3, ZFMISC_1:106; :: thesis: verum