let e be epsilon Ordinal; :: thesis: ex a being ordinal number st e = 1 -Veblen a
set U = Tarski-Class (e \/ omega);
A0: omega in Tarski-Class (e \/ omega) by Unc1;
( 0-element_of (Tarski-Class (e \/ omega)) = 0 & 1-element_of (Tarski-Class (e \/ omega)) = 1 ) ;
then reconsider f = ((Tarski-Class (e \/ omega)) -Veblen) . 0, g = ((Tarski-Class (e \/ omega)) -Veblen) . 1 as normal Ordinal-Sequence of (Tarski-Class (e \/ omega)) by A0, Th23;
A1: g = criticals ((Tarski-Class (e \/ omega)) exp omega) by Th12
.= criticals f by V ;
A2: f . e = 0 -Veblen e
.= exp (omega,e) by Th10
.= e by ORDINAL5:def 5 ;
A3: dom f = On (Tarski-Class (e \/ omega)) by FUNCT_2:def 1;
( e c= e \/ omega & e \/ omega in Tarski-Class (e \/ omega) ) by CLASSES1:2, XBOOLE_1:7;
then A5: e in Tarski-Class (e \/ omega) by CLASSES1:def 1;
then e in On (Tarski-Class (e \/ omega)) by ORDINAL1:def 9;
then e is_a_fixpoint_of f by A2, A3, ABIAN:def 3;
then consider a being ordinal number such that
A4: ( a in dom (criticals f) & e = (criticals f) . a ) by Th06;
take a ; :: thesis: e = 1 -Veblen a
set W = Tarski-Class (a \/ omega);
A6: ( a c= a \/ omega & a \/ omega in Tarski-Class (a \/ omega) ) by CLASSES1:2, XBOOLE_1:7;
a c= e by A4, ORDINAL4:10;
then ( omega in Tarski-Class (a \/ omega) & a in Tarski-Class (a \/ omega) & a in Tarski-Class (e \/ omega) & 1-element_of (Tarski-Class (e \/ omega)) = 1-element_of (Tarski-Class (a \/ omega)) ) by A5, A6, Unc1, CLASSES1:def 1;
hence e = 1 -Veblen a by A0, A1, A4, Th25; :: thesis: verum