A4: F₃() ~ reduces F₂(),F₁() by A2, REWRITE1:24;
A5: for y, z being set st F₃() ~ reduces F₂(),y & [y,z] in F₃() ~ & P₁[y] holds
P₁[z]

proof

let y, z be set ; :: thesis: ( F₃() ~ reduces F₂(),y & [y,z] in F₃() ~ & P₁[y] implies P₁[z] )
assume F₃() ~ reduces F₂(),y ; :: thesis: ( not [y,z] in F₃() ~ or not P₁[y] or P₁[z] )
assume [y,z] in F₃() ~ ; :: thesis: ( not P₁[y] or P₁[z] )
then [z,y] in F₃() by RELAT_1:def 7;
hence ( not P₁[y] or P₁[z] ) by A3; :: thesis: verum

end;

thus P₁[F₁()] from MSAFREE4:sch 5(A1, A4, A5); :: thesis: verum