thus ( F₃() in F₁() implies P₁[F₃()] ) :: thesis: ( P₁[F₃()] implies F₃() in F₁() )

proof

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

end;

assume P₁[F₃()] ; :: thesis: F₃() in F₁()
hence F₃() in F₁() by A1; :: thesis: verum