let a be Ordinal; :: thesis: ( 1 -Veblen a = epsilon_ a implies 1 -Veblen (succ a) = epsilon_ (succ a) )
assume A1: 1 -Veblen a = epsilon_ a ; :: thesis: 1 -Veblen (succ a) = epsilon_ (succ a)
consider b being Ordinal such that
A2: 1 -Veblen (succ a) = epsilon_ b by Th75, ORDINAL5:51;
consider c being Ordinal such that
A3: epsilon_ (succ a) = 1 -Veblen c by Th76;
A4: a in succ a by ORDINAL1:6;
epsilon_ a in epsilon_ (succ a) by ORDINAL1:6, ORDINAL5:44;
then a in c by A1, A3, Th72;
then succ a c= c by ORDINAL1:21;
hence 1 -Veblen (succ a) c= epsilon_ (succ a) by A3, Th71; :: according to XBOOLE_0:def 10 :: thesis: epsilon_ (succ a) c= 1 -Veblen (succ a)
assume epsilon_ (succ a) c/= 1 -Veblen (succ a) ; :: thesis: contradiction
then epsilon_ b in epsilon_ (succ a) by A2, Th4;
then b in succ a by Th12;
then b c= a by ORDINAL1:22;
then epsilon_ b c= epsilon_ a by Th11;
then succ a c= a by A1, A2, Th71;
then a in a by A4;
hence contradiction ; :: thesis: verum