( 0 in {0 ,1,2} & 0 in NAT ) by ENUMSET1:def 1;
hence [0 ,0 ] is MP-conective by ZFMISC_1:106; :: thesis: verum