ex a being set st
( a in F₂() & P₁[a] & ( for b being set st b in F₂() & P₁[b] & b c= a holds
b = a ) )

A1: ( F₁() in F₂() & P₁[F₁()] ) and
A2: F₁() is finite