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