:: deftheorem Def2 defines thin_cylinder PETRI_2:def 2 :
for A being non empty set
for B being set
for b₃ being non empty Subset of (Funcs (B,A)) holds
( b₃ is thin_cylinder of A,B iff ex Bo being Subset of B ex yo being Function of Bo,A st
( Bo is finite & b₃ = cylinder0 (A,B,Bo,yo) ) );