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