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:
{ x where x is Element of the carrier of F1() : P1[x] } is Subset of the carrier of F1()
from DOMAIN_1:sch 7();
F2() in { x where x is Element of the carrier of F1() : P1[x] }
by A1;
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, Def2;
then consider a being set such that
A4:
( a in Z & the InternalRel of F1() -Seg a misses Z )
by WELLORD1:def 3;
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 a' being Element of the carrier of F1() st
( a' = a & P1[a'] )
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 A5:
( 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 A5, WELLORD1:def 1;
hence
contradiction
by A4, XBOOLE_0:3; :: thesis: verum