consider b being Ordinal such that
A1: 1 -Veblen 0 = epsilon_ b by Th75, ORDINAL5:51;
consider a being Ordinal such that
A2: epsilon_ 0 = 1 -Veblen a by Th76;

now :: thesis: not b <> 0

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

end;

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