set bX = bool F₁();
consider R being Relation such that
A3: R well_orders F₁() by WELLORD2:17;
R /\ [:F₁(),F₁():] c= [:F₁(),F₁():] by XBOOLE_1:17;
then reconsider R2 = R |_2 F₁() as Relation of F₁() by WELLORD1:def 6;
reconsider RS = RelStr(# F₁(),R2 #) as non empty RelStr ;
set cRS = the carrier of RS;
defpred S₁[ object , object , object ] means for p being Element of F₁()
for f being PartFunc of the carrier of RS,(bool F₁()) st $1 = p & $2 = f holds
( ( ( for q being Element of F₁() st q in union (rng f) holds
P₁[p,q] ) implies $3 = (union (rng f)) \/ {p} ) & ( ex q being Element of F₁() st
( q in union (rng f) & P₁[p,q] ) implies $3 = union (rng f) ) );
A4: for x, y being object st x in the carrier of RS & y in PFuncs ( the carrier of RS,(bool F₁())) holds
ex z being object st
( z in bool F₁() & S₁[x,y,z] )

let x, y be object ; :: thesis:
assume that
A5: x in the carrier of RS and
A6: y in PFuncs ( the carrier of RS,(bool F₁())) ; :: thesis:
reconsider f = y as PartFunc of the carrier of RS,(bool F₁()) by A6, PARTFUN1:46;
reconsider p = x as Element of F₁() by A5;

suppose A7: for q being Element of F₁() st q in union (rng f) holds
P₁[p,q] ; :: thesis:

take (union (rng f)) \/ {p} ; :: thesis:
thus ( (union (rng f)) \/ {p} in bool F₁() & S₁[x,y,(union (rng f)) \/ {p}] ) by A7; :: thesis:

end;

suppose A8: ex q being Element of F₁() st
( q in union (rng f) & P₁[p,q] ) ; :: thesis:

take union (rng f) ; :: thesis:
thus ( union (rng f) in bool F₁() & S₁[x,y, union (rng f)] ) by A8; :: thesis:

end;

consider h being Function of [: the carrier of RS,(PFuncs ( the carrier of RS,(bool F₁()))):],(bool F₁()) such that
A9: for x, y being object st x in the carrier of RS & y in PFuncs ( the carrier of RS,(bool F₁())) holds
S₁[x,y,h . (x,y)] from BINOP_1:sch 1(A4);
set IRS = the InternalRel of RS;
A10: R2 well_orders F₁() by A3, PCOMPS_2:1;
then R2 is_well_founded_in F₁() by WELLORD1:def 5;
then A11: RS is well_founded by WELLFND1:def 2;
then consider f being Function of the carrier of RS,(bool F₁()) such that
A12: f is_recursively_expressed_by h by WELLFND1:11;
defpred S₂[ set ] means ( f . $1 c= ( the InternalRel of RS -Seg $1) \/ {$1} & ( $1 in f . $1 implies for r being Element of F₁() st r in union (rng (f | ( the InternalRel of RS -Seg $1))) holds
P₁[$1,r] ) & ( not $1 in f . $1 implies ex r being Element of F₁() st
( r in union (rng (f | ( the InternalRel of RS -Seg $1))) & P₁[$1,r] ) ) );
reconsider rngf = rng f as Subset of (bool F₁()) ;
take A = union rngf; :: thesis:
A13: field R2 = F₁() by A3, PCOMPS_2:1;
then A14: R2 is well-ordering by A10, WELLORD1:4;
A15: for x being Element of RS st ( for y being Element of RS st y <> x & [y,x] in the InternalRel of RS holds
S₂[y] ) holds
S₂[x]

proof

let x be Element of RS; :: thesis:
assume A16: for y being Element of RS st y <> x & [y,x] in the InternalRel of RS holds
S₂[y] ; :: thesis:
set fIx = f | ( the InternalRel of RS -Seg x);
A17: union (rng (f | ( the InternalRel of RS -Seg x))) c= the InternalRel of RS -Seg x

proof

end;

A27: f | ( the InternalRel of RS -Seg x) in PFuncs ( the carrier of RS,(bool F₁())) by PARTFUN1:45;
A28: f . x = h . (x,(f | ( the InternalRel of RS -Seg x))) by A12, WELLFND1:def 5;

per cases ;

suppose A29: for q being Element of F₁() st q in union (rng (f | ( the InternalRel of RS -Seg x))) holds
P₁[x,q] ; :: thesis:

then A30: f . x = (union (rng (f | ( the InternalRel of RS -Seg x)))) \/ {x} by A9, A28, A27;
hence f . x c= ( the InternalRel of RS -Seg x) \/ {x} by A17, XBOOLE_1:9; :: thesis:
thus ( x in f . x implies for r being Element of F₁() st r in union (rng (f | ( the InternalRel of RS -Seg x))) holds
P₁[x,r] ) by A29; :: thesis:
A31: x in {x} by TARSKI:def 1;
assume not x in f . x ; :: thesis:
hence ex r being Element of F₁() st
( r in union (rng (f | ( the InternalRel of RS -Seg x))) & P₁[x,r] ) by A30, A31, XBOOLE_0:def 3; :: thesis:

end;

suppose A32: ex q being Element of F₁() st
( q in union (rng (f | ( the InternalRel of RS -Seg x))) & P₁[x,q] ) ; :: thesis:

then A33: f . x c= the InternalRel of RS -Seg x by A9, A17, A28, A27;
the InternalRel of RS -Seg x c= ( the InternalRel of RS -Seg x) \/ {x} by XBOOLE_1:7;
hence f . x c= ( the InternalRel of RS -Seg x) \/ {x} by A33; :: thesis:
thus ( ( x in f . x implies for r being Element of F₁() st r in union (rng (f | ( the InternalRel of RS -Seg x))) holds
P₁[x,r] ) & ( not x in f . x implies ex r being Element of F₁() st
( r in union (rng (f | ( the InternalRel of RS -Seg x))) & P₁[x,r] ) ) ) by A32, A33, WELLORD1:1; :: thesis:

end;

A34: for x being Element of RS holds S₂[x] from WELLFND1:sch 3(A15, A11);
thus for x, y being Element of F₁() st x in A & y in A & x <> y holds
P₁[x,y] :: thesis:

proof

A35: now :: thesis:

let x be Element of F₁(); :: thesis:
assume x in A ; :: thesis:
then consider y being set such that
A36: x in y and
A37: y in rng f by TARSKI:def 4;
defpred S₃[ set ] means x in f . $1;
consider z being object such that
A38: z in dom f and
A39: f . z = y by A37, FUNCT_1:def 3;
reconsider z = z as Element of RS by A38;
A40: S₃[z] by A36, A39;
consider p being Element of RS such that
A41: S₃[p] and
A42: for q being Element of RS holds
( not p <> q or not S₃[q] or not [q,p] in the InternalRel of RS ) from WELLFND1:sch 2(A40, A11);
p = x

proof

set fIp = f | ( the InternalRel of RS -Seg p);
A43: f | ( the InternalRel of RS -Seg p) in PFuncs ( the carrier of RS,(bool F₁())) by PARTFUN1:45;
A44: f . p = h . (p,(f | ( the InternalRel of RS -Seg p))) by A12, WELLFND1:def 5;
assume A45: p <> x ; :: thesis:

now :: thesis:

per cases ;

suppose A46: for q being Element of F₁() st q in union (rng (f | ( the InternalRel of RS -Seg p))) holds
P₁[p,q] ; :: thesis:

A47: not x in {p} by A45, TARSKI:def 1;
f . p = (union (rng (f | ( the InternalRel of RS -Seg p)))) \/ {p} by A9, A44, A43, A46;
hence x in union (rng (f | ( the InternalRel of RS -Seg p))) by A41, A47, XBOOLE_0:def 3; :: thesis:

end;

suppose ex q being Element of F₁() st
( q in union (rng (f | ( the InternalRel of RS -Seg p))) & P₁[p,q] ) ; :: thesis:

hence x in union (rng (f | ( the InternalRel of RS -Seg p))) by A9, A41, A44, A43; :: thesis:

end;

then consider y9 being set such that
A48: x in y9 and
A49: y9 in rng (f | ( the InternalRel of RS -Seg p)) by TARSKI:def 4;
consider z9 being object such that
A50: z9 in dom (f | ( the InternalRel of RS -Seg p)) and
A51: (f | ( the InternalRel of RS -Seg p)) . z9 = y9 by A49, FUNCT_1:def 3;
reconsider z9 = z9 as Point of RS by A50;
A52: z9 in the InternalRel of RS -Seg p by A50, RELAT_1:57;
then A53: z9 <> p by WELLORD1:1;
A54: [z9,p] in the InternalRel of RS by A52, WELLORD1:1;
S₃[z9] by A48, A50, A51, FUNCT_1:47;
hence contradiction by A42, A53, A54; :: thesis:

end;

hence x in f . x by A41; :: thesis:

end;

A55: now :: thesis:

end;

let x, y be Element of F₁(); :: thesis:
assume that
A65: x in A and
A66: y in A and
A67: x <> y ; :: thesis:
R2 well_orders F₁() by A3, PCOMPS_2:1;
then R2 is_connected_in F₁() by WELLORD1:def 5;
then ( [x,y] in the InternalRel of RS or [y,x] in the InternalRel of RS ) by A67, RELAT_2:def 6;
then ( P₁[x,y] or P₁[y,x] ) by A55, A65, A66, A67;
hence P₁[x,y] by A1; :: thesis:

end;

let x be Element of F₁(); :: thesis:

per cases ;

suppose A68: x in A ; :: thesis:

take x ; :: thesis:
thus ( x in A & P₁[x,x] ) by A2, A68; :: thesis:

end;

suppose A69: not x in A ; :: thesis:

not x in f . x

proof

dom f = the carrier of RS by FUNCT_2:def 1;
then A70: f . x in rng f by FUNCT_1:def 3;
assume x in f . x ; :: thesis:
hence contradiction by A69, A70, TARSKI:def 4; :: thesis:

end;

then consider r being Element of F₁() such that
A71: r in union (rng (f | ( the InternalRel of RS -Seg x))) and
A72: P₁[x,r] by A34;
take r ; :: thesis:
union (rng (f | ( the InternalRel of RS -Seg x))) c= A by RELAT_1:70, ZFMISC_1:77;
hence ( r in A & P₁[x,r] ) by A71, A72; :: thesis:

end;