:: deftheorem defines M_3 YELLOW11:def 2 :
M_3 = InclPoset {0,1,(2 \ 1),(3 \ 2),3};