consider b being ordinal number such that
A0: 1 -Veblen 0 = epsilon_ b by Th13, ORDINAL5:51;
consider a being ordinal number such that
A1: epsilon_ 0 = 1 -Veblen a by Th14;

now

assume b <> 0 ; :: thesis: contradiction
then epsilon_ 0 in epsilon_ b by ORDINAL3:8, ORDINAL5:44;
hence contradiction by A0, A1, Th15a; :: thesis: verum

end;

hence 1 -Veblen 0 = epsilon_ 0 by A0; :: thesis: verum