:: deftheorem defines Colored-states PETRI_3:def 10 :
for CPN being Colored-PT-net holds Colored-states CPN = { e where e is color-count of CPN : verum } ;