assume not MP-conectives misses MP-variables ; :: thesis: contradiction
then consider x being set such that
A1: x in [:{0 ,1,2},NAT :] and
A2: x in [:{3},NAT :] by XBOOLE_0:3;
consider x1, x2 being set such that
A3: x1 in {0 ,1,2} and
x2 in NAT and
A4: x = [x1,x2] by A1, ZFMISC_1:def 2;
x1 = 3 by A2, A4, ZFMISC_1:128;
hence contradiction by A3, ENUMSET1:def 1; :: thesis: verum