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;
00: S₁[ 0 ] by Th16;
01: for b being ordinal number st S₁[b] holds
S₁[ succ b] by Th17;
02: 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 Th18;
for b being ordinal number holds S₁[b] from ORDINAL2:sch 1(00, 01, 02);
hence 1 -Veblen a = epsilon_ a ; :: thesis: verum