thus ( F₄() in F₅(F₃()) implies for b being Element of F₂() st b in F₃() holds
P₁[F₄(),b] ) :: thesis: ( ( for b being Element of F₂() st b in F₃() holds
P₁[F₄(),b] ) implies F₄() in F₅(F₃()) )

proof

defpred S₁[ set ] means P₂[$1,F₃()];
assume F₄() in F₅(F₃()) ; :: thesis: for b being Element of F₂() st b in F₃() holds
P₁[F₄(),b]
then A3: F₄() in { a where a is Element of F₁() : S₁[a] } by A1;
S₁[F₄()] from LMOD_7:sch 6(A3);
hence for b being Element of F₂() st b in F₃() holds
P₁[F₄(),b] by A2; :: thesis: verum

end;

assume for b being Element of F₂() st b in F₃() holds
P₁[F₄(),b] ; :: thesis: F₄() in F₅(F₃())
hence F₄() in F₅(F₃()) by A1, A2; :: thesis: verum