set c = the carrier of F1();
set r = the InternalRel of F1();
set Z = { x where x is Element of the carrier of F1() : P1[x] } ;
A3: F2() in { x where x is Element of the carrier of F1() : P1[x] } by A1;
{ x where x is Element of the carrier of F1() : P1[x] } is Subset of the carrier of F1() from then reconsider Z = { x where x is Element of the carrier of F1() : P1[x] } as non empty Subset of the carrier of F1() by A3;
the InternalRel of F1() is_well_founded_in the carrier of F1() by A2;
then consider a being object such that
A4: a in Z and
A5: the InternalRel of F1() -Seg a misses Z ;
reconsider a = a as Element of F1() by A4;
take a ; :: thesis: ( P1[a] & ( for y being Element of F1() holds
( not a <> y or not P1[y] or not [y,a] in the InternalRel of F1() ) ) )

ex a9 being Element of the carrier of F1() st
( a9 = a & P1[a9] ) by A4;
hence P1[a] ; :: thesis: for y being Element of F1() holds
( not a <> y or not P1[y] or not [y,a] in the InternalRel of F1() )

given y being Element of F1() such that A6: ( a <> y & P1[y] & [y,a] in the InternalRel of F1() ) ; :: thesis: contradiction
( y in Z & y in the InternalRel of F1() -Seg a ) by ;
hence contradiction by A5, XBOOLE_0:3; :: thesis: verum