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