let e be epsilon Ordinal; :: thesis: ex a being Ordinal st e = 1 -Veblen a
set U = Tarski-Class (e \/ omega);
A1: omega in Tarski-Class (e \/ omega) by Th57;
( 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 A1, Th62;
A2: g = criticals ((Tarski-Class (e \/ omega)) exp omega) by Th74
.= criticals f by Def15 ;
A3: f . e = 0 -Veblen e
.= exp (omega,e) by Th68
.= e by ORDINAL5:def 5 ;
A4: 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 A3, A4;
then consider a being Ordinal such that
A6: ( a in dom (criticals f) & e = (criticals f) . a ) by Th33;
take a ; :: thesis: e = 1 -Veblen a
set W = Tarski-Class (a \/ omega);
A7: ( a c= a \/ omega & a \/ omega in Tarski-Class (a \/ omega) ) by CLASSES1:2, XBOOLE_1:7;
a c= e by A6, 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, A7, Th57, CLASSES1:def 1;
hence e = 1 -Veblen a by A1, A2, A6, Th64; :: thesis: verum