scheme :: POLYFORM:sch 1
ChainEx{ F₁() -> polyhedron, F₂() -> Integer, P₁[ Element of F₂() -polytopes F₁()] } :

ex c being Subset of (F₂() -polytopes F₁()) st
for x being Element of F₂() -polytopes F₁() holds
( x in c iff ( P₁[x] & x in F₂() -polytopes F₁() ) )