let l be limit_ordinal non empty Ordinal; :: thesis: ( ( for a being Ordinal st a in l holds
1 -Veblen a = epsilon_ a ) implies 1 -Veblen l = epsilon_ l )
assume A1: for a being Ordinal st a in l holds
1 -Veblen a = epsilon_ a ; :: thesis: 1 -Veblen l = epsilon_ l
set U = Tarski-Class (l \/ omega);
0 in l by ORDINAL3:8;
then omega c= l by ORDINAL1:def 11;
then l \/ omega = l by XBOOLE_1:12;
then A2: l in Tarski-Class (l \/ omega) by CLASSES1:2;
A3: omega in Tarski-Class (l \/ omega) by Th57;
1-element_of (Tarski-Class (l \/ omega)) = 1 ;
then reconsider g = ((Tarski-Class (l \/ omega)) -Veblen) . 1 as normal Ordinal-Sequence of (Tarski-Class (l \/ omega)) by A3, Th62;
reconsider o = omega as non trivial Ordinal of Tarski-Class (l \/ omega) by Th57;
set f = (Tarski-Class (l \/ omega)) exp o;
A4: g = criticals ((Tarski-Class (l \/ omega)) exp o) by Th74;
A5: dom g = On (Tarski-Class (l \/ omega)) by FUNCT_2:def 1;
then A6: l in dom g by A2, ORDINAL1:def 9;
then A7: g . l = Union (g | l) by A4, Th39
.= union (rng (g | l)) ;
l c= dom g by A6, ORDINAL1:def 2;
then A8: dom (g | l) = l by RELAT_1:62;

now :: thesis: for x being set st x in rng (g | l) holds
x c= epsilon_ l

let x be set ; :: thesis: ( x in rng (g | l) implies x c= epsilon_ l )
assume x in rng (g | l) ; :: thesis: x c= epsilon_ l
then consider y being object such that
A9: ( y in dom (g | l) & x = (g | l) . y ) by FUNCT_1:def 3;
reconsider y = y as Ordinal by A9;
A10: x = g . y by A9, FUNCT_1:47;
y in dom g by A6, A8, A9, ORDINAL1:10;
then ( y in Tarski-Class (l \/ omega) & 1-element_of (Tarski-Class (l \/ omega)) in Tarski-Class (l \/ omega) ) by A5, ORDINAL1:def 9;
then x = 1 -Veblen y by A3, A10, Th67;
then x = epsilon_ y by A1, A8, A9;
then x in epsilon_ l by A8, A9, Th12;
hence x c= epsilon_ l by ORDINAL1:def 2; :: thesis: verum

end;

hence 1 -Veblen l c= epsilon_ l by A7, ZFMISC_1:76; :: according to XBOOLE_0:def 10 :: thesis: epsilon_ l c= 1 -Veblen l
let a be Ordinal; :: according to ORDINAL1:def 5 :: thesis: ( not a in epsilon_ l or a in 1 -Veblen l )
assume a in epsilon_ l ; :: thesis: a in 1 -Veblen l
then consider b being Ordinal such that
A11: ( b in l & a in epsilon_ b ) by ORDINAL5:47;
epsilon_ b = 1 -Veblen b by A1, A11;
then epsilon_ b in 1 -Veblen l by A11, Th72;
hence a in 1 -Veblen l by A11, ORDINAL1:10; :: thesis: verum