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