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