let nt be NonTerminal of SCM-AE; :: thesis: not not nt = [0,0] & ... & not nt = [0,4]

consider x, y being object 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 Nat such that

A5: y = n and

A6: n < 5 by A2, Lm2;

5 = 4 + 1 ;

then n <= 4 by A6, NAT_1:13;

then not not n = 0 & ... & not n = 4 ;

hence not not nt = [0,0] & ... & not nt = [0,4] by A3, A4, A5; :: thesis: verum

consider x, y being object 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 Nat such that

A5: y = n and

A6: n < 5 by A2, Lm2;

5 = 4 + 1 ;

then n <= 4 by A6, NAT_1:13;

then not not n = 0 & ... & not n = 4 ;

hence not not nt = [0,0] & ... & not nt = [0,4] by A3, A4, A5; :: thesis: verum