A4:
F3() ~ reduces F2(),F1()
by A2, REWRITE1:24;
A5:
for y, z being set st F3() ~ reduces F2(),y & [y,z] in F3() ~ & P1[y] holds
P1[z]
proof
let y,
z be
set ;
( F3() ~ reduces F2(),y & [y,z] in F3() ~ & P1[y] implies P1[z] )
assume
F3()
~ reduces F2(),
y
;
( not [y,z] in F3() ~ or not P1[y] or P1[z] )
assume
[y,z] in F3()
~
;
( not P1[y] or P1[z] )
then
[z,y] in F3()
by RELAT_1:def 7;
hence
( not
P1[
y] or
P1[
z] )
by A3;
verum
end;
thus
P1[F1()]
from MSAFREE4:sch 5(A1, A4, A5); verum