:: deftheorem defines thin_cylinders PETRI_2:def 3 :
for A being non empty set
for B being set holds thin_cylinders (A,B) = { D where D is Subset of (Funcs (B,A)) : D is thin_cylinder of A,B } ;