scheme :: DILWORTH:sch 1
FraenkelFinCard1{ F₁() -> non empty finite set , P₁[ set ], F₂() -> finite set , F₃( set ) -> set } :

card F₂() <= card F₁()

provided

A1: F₂() = { F₃(w) where w is Element of F₁() : P₁[w] }