set c = the carrier of F_{1}();

set r = the InternalRel of F_{1}();

set Z = { x where x is Element of the carrier of F_{1}() : P_{1}[x] } ;

A3: F_{2}() in { x where x is Element of the carrier of F_{1}() : P_{1}[x] }
by A1;

{ x where x is Element of the carrier of F_{1}() : P_{1}[x] } is Subset of the carrier of F_{1}()
from DOMAIN_1:sch 7();

then reconsider Z = { x where x is Element of the carrier of F_{1}() : P_{1}[x] } as non empty Subset of the carrier of F_{1}() by A3;

the InternalRel of F_{1}() is_well_founded_in the carrier of F_{1}()
by A2;

then consider a being object such that

A4: a in Z and

A5: the InternalRel of F_{1}() -Seg a misses Z
;

reconsider a = a as Element of F_{1}() by A4;

take a ; :: thesis: ( P_{1}[a] & ( for y being Element of F_{1}() holds

( not a <> y or not P_{1}[y] or not [y,a] in the InternalRel of F_{1}() ) ) )

ex a9 being Element of the carrier of F_{1}() st

( a9 = a & P_{1}[a9] )
by A4;

hence P_{1}[a]
; :: thesis: for y being Element of F_{1}() holds

( not a <> y or not P_{1}[y] or not [y,a] in the InternalRel of F_{1}() )

given y being Element of F_{1}() such that A6:
( a <> y & P_{1}[y] & [y,a] in the InternalRel of F_{1}() )
; :: thesis: contradiction

( y in Z & y in the InternalRel of F_{1}() -Seg a )
by A6, WELLORD1:1;

hence contradiction by A5, XBOOLE_0:3; :: thesis: verum

set r = the InternalRel of F

set Z = { x where x is Element of the carrier of F

A3: F

{ x where x is Element of the carrier of F

then reconsider Z = { x where x is Element of the carrier of F

the InternalRel of F

then consider a being object such that

A4: a in Z and

A5: the InternalRel of F

reconsider a = a as Element of F

take a ; :: thesis: ( P

( not a <> y or not P

ex a9 being Element of the carrier of F

( a9 = a & P

hence P

( not a <> y or not P

given y being Element of F

( y in Z & y in the InternalRel of F

hence contradiction by A5, XBOOLE_0:3; :: thesis: verum