:: deftheorem defines loc PETRI_2:def 6 :
for A being non trivial set
for B being set
for D being thin_cylinder of A,B
for b₄ being finite Subset of B holds
( b₄ = loc D iff ex Bo being Subset of B ex yo being Function of Bo,A st
( Bo is finite & D = { y where y is Function of B,A : y | Bo = yo } & b₄ = Bo ) );