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₁() ) )