A3: F₃() in { a where a is Element of F₂() : P₁[a] } by A1, A2;
thus P₁[F₃()] from LMOD_7:sch 6(A3); :: thesis: verum