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 DOMAIN_1:sch 7();
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
; ( 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]
; 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() )
; contradiction
( y in Z & y in the InternalRel of F1() -Seg a )
by A6, WELLORD1:1;
hence
contradiction
by A5, XBOOLE_0:3; verum