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