ex a being Element of F₁() st
( F₂() = a & P₁[a] ) by A1;
hence P₁[F₂()] ; :: thesis: verum