let a be Ordinal; :: 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 Lm4;
A2: for b being Ordinal st S₁[b] holds
S₁[ succ b] by Lm5;
A3: for b being Ordinal st b <> 0 & b is limit_ordinal & ( for c being Ordinal st c in b holds
S₁[c] ) holds
S₁[b] by Lm6;
for b being Ordinal holds S₁[b] from ORDINAL2:sch 1(A1, A2, A3);
hence 1 -Veblen a = epsilon_ a ; :: thesis: verum