let a be ordinal number ; :: thesis: 1 -Veblen a = epsilon_ a
set U = Tarski-Class (a \/ omega);
defpred S₁[ Ordinal] means 1 -Veblen $1 = epsilon_ $1;
A1: S₁[ 0 ] by Lm5;
A2: for b being ordinal number st S₁[b] holds
S₁[ succ b] by Lm6;
A3: for b being ordinal number st b <> {} & b is limit_ordinal & ( for c being ordinal number st c in b holds
S₁[c] ) holds
S₁[b] by Lm7;
for b being ordinal number holds S₁[b] from ORDINAL2:sch 1(A1, A2, A3);
hence 1 -Veblen a = epsilon_ a ; :: thesis: verum