assume not MP-conectives misses MP-variables ; :: thesis: contradiction
then consider x being object such that
A1: x in [:{0,1,2},NAT:] and
A2: x in [:{3},NAT:] by XBOOLE_0:3;
consider x1, x2 being object 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:105;
hence contradiction by A3, ENUMSET1:def 1; :: thesis: verum