let a be Ordinal; :: thesis: 1 -Veblen a is epsilon
set U = Tarski-Class (a \/ omega);
0 -Veblen (1 -Veblen a) = (succ 0) -Veblen a by Th69;
hence exp (omega,(1 -Veblen a)) = 1 -Veblen a by Th68; :: according to ORDINAL5:def 5 :: thesis: verum