assume A3: for A being Ordinal holds not F₁(A) = A ; :: thesis: contradiction
deffunc H₁( Ordinal, Ordinal) -> Ordinal = F₁($2);
deffunc H₂( Ordinal, T-Sequence) -> set = {} ;
consider phi being Ordinal-Sequence such that
A4: dom phi = omega and
A5: ( {} in omega implies phi . {} = F₁({} ) ) and
A6: for A being Ordinal st succ A in omega holds
phi . (succ A) = H₁(A,phi . A) and
for A being Ordinal st A in omega & A <> {} & A is limit_ordinal holds
phi . A = H₂(A,phi | A) from ORDINAL2:sch 11();

A7: now

defpred S₁[ Ordinal] means not $1 c= F₁($1);
assume A8: ex A being Ordinal st S₁[A] ; :: thesis: contradiction
consider A being Ordinal such that
A9: S₁[A] and
A10: for B being Ordinal st S₁[B] holds
A c= B from ORDINAL1:sch 1(A8);
F₁(F₁(A)) in F₁(A) by A1, A9, ORDINAL1:26;
then not F₁(A) c= F₁(F₁(A)) by ORDINAL1:7;
hence contradiction by A9, A10; :: thesis: verum

end;

A11: now

let A be Ordinal; :: thesis: A in F₁(A)
( A c= F₁(A) & A <> F₁(A) ) by A3, A7;
then A c< F₁(A) by XBOOLE_0:def 8;
hence A in F₁(A) by ORDINAL1:21; :: thesis: verum

end;

A12: phi is increasing

proof

let A be Ordinal; :: according to ORDINAL2:def 16 :: thesis: for b₁ being set holds
( not A in b₁ or not b₁ in dom phi or phi . A in phi . b₁ )
let B be Ordinal; :: thesis: ( not A in B or not B in dom phi or phi . A in phi . B )
assume A13: ( A in B & B in dom phi ) ; :: thesis: phi . A in phi . B
then A14: ex C being Ordinal st
( B = A +^ C & C <> {} ) by ORDINAL3:31;
defpred S₁[ Ordinal] means ( A +^ $1 in omega & $1 <> {} implies phi . A in phi . (A +^ $1) );
A15: S₁[ {} ] ;
A16: for C being Ordinal st S₁[C] holds
S₁[ succ C]

proof

let C be Ordinal; :: thesis: ( S₁[C] implies S₁[ succ C] )
assume that
A17: ( A +^ C in omega & C <> {} implies phi . A in phi . (A +^ C) ) and
A18: ( A +^ (succ C) in omega & succ C <> {} ) ; :: thesis: phi . A in phi . (A +^ (succ C))
A19: ( A +^ C in succ (A +^ C) & A +^ (succ C) = succ (A +^ C) ) by ORDINAL1:10, ORDINAL2:45;
reconsider D = phi . (A +^ C) as Ordinal ;
( phi . (A +^ (succ C)) = F₁(D) & D in F₁(D) & A +^ {} = A ) by A6, A11, A18, A19, ORDINAL2:44;
hence phi . A in phi . (A +^ (succ C)) by A17, A18, A19, ORDINAL1:19; :: thesis: verum

end;

A20: for B being Ordinal st B <> {} & B is limit_ordinal & ( for C being Ordinal st C in B holds
S₁[C] ) holds
S₁[B]

proof

let B be Ordinal; :: thesis: ( B <> {} & B is limit_ordinal & ( for C being Ordinal st C in B holds
S₁[C] ) implies S₁[B] )
assume that
A21: ( B <> {} & B is limit_ordinal ) and
for C being Ordinal st C in B & A +^ C in omega & C <> {} holds
phi . A in phi . (A +^ C) and
A22: ( A +^ B in omega & B <> {} ) ; :: thesis: phi . A in phi . (A +^ B)
A +^ B <> {} by A22, ORDINAL3:29;
then ( A +^ B is limit_ordinal & {} in A +^ B ) by A21, ORDINAL3:10, ORDINAL3:32;
then omega c= A +^ B by ORDINAL1:def 12;
hence phi . A in phi . (A +^ B) by A22, ORDINAL1:7; :: thesis: verum

end;

for C being Ordinal holds S₁[C] from ORDINAL2:sch 1(A15, A16, A20);
hence phi . A in phi . B by A4, A13, A14; :: thesis: verum

end;

deffunc H₃( Ordinal) -> Ordinal = F₁($1);
consider fi being Ordinal-Sequence such that
A23: ( dom fi = sup phi & ( for A being Ordinal st A in sup phi holds
fi . A = H₃(A) ) ) from ORDINAL2:sch 3();
( H₃( {} ) in rng phi & sup (rng phi) = sup phi ) by A4, A5, Lm1, FUNCT_1:def 5;
then A24: ( sup phi <> {} & sup phi is limit_ordinal ) by A4, A12, Lm2, Th16, ORDINAL2:27;
then A25: H₃( sup phi) is_limes_of fi by A2, A23;
fi is increasing

proof

let A be Ordinal; :: according to ORDINAL2:def 16 :: thesis: for b₁ being set holds
( not A in b₁ or not b₁ in dom fi or fi . A in fi . b₁ )
let B be Ordinal; :: thesis: ( not A in B or not B in dom fi or fi . A in fi . B )
assume A26: ( A in B & B in dom fi ) ; :: thesis: fi . A in fi . B
then ( fi . A = H₃(A) & fi . B = H₃(B) ) by A23, ORDINAL1:19;
hence fi . A in fi . B by A1, A26; :: thesis: verum

end;

then A27: sup fi = lim fi by A23, A24, Th8
.= H₃( sup phi) by A25, ORDINAL2:def 14 ;
sup fi c= sup phi

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in sup fi or x in sup phi )
assume A28: x in sup fi ; :: thesis: x in sup phi
then reconsider A = x as Ordinal ;
consider B being Ordinal such that
A29: ( B in rng fi & A c= B ) by A28, ORDINAL2:29;
consider y being set such that
A30: ( y in dom fi & B = fi . y ) by A29, FUNCT_1:def 5;
reconsider y = y as Ordinal by A30;
consider C being Ordinal such that
A31: ( C in rng phi & y c= C ) by A23, A30, ORDINAL2:29;
consider z being set such that
A32: ( z in dom phi & C = phi . z ) by A31, FUNCT_1:def 5;
reconsider z = z as Ordinal by A32;
succ z in omega by A4, A32, Lm2, ORDINAL1:41;
then A33: ( phi . (succ z) = H₃(C) & phi . (succ z) in rng phi & B = H₃(y) ) by A4, A6, A23, A30, A32, FUNCT_1:def 5;
( y c< C iff ( y <> C & y c= C ) ) by XBOOLE_0:def 8;
then ( H₃(y) in H₃(C) or y = C ) by A1, A31, ORDINAL1:21;
then ( B c= H₃(C) & H₃(C) in sup phi ) by A33, ORDINAL1:def 2, ORDINAL2:27;
then B in sup phi by ORDINAL1:22;
hence x in sup phi by A29, ORDINAL1:22; :: thesis: verum

end;

hence contradiction by A11, A27, ORDINAL1:7; :: thesis: verum