let a be ordinal number ; :: thesis: ( 1 -Veblen a = epsilon_ a implies 1 -Veblen (succ a) = epsilon_ (succ a) )
assume Z0: 1 -Veblen a = epsilon_ a ; :: thesis: 1 -Veblen (succ a) = epsilon_ (succ a)
consider b being ordinal number such that
A0: 1 -Veblen (succ a) = epsilon_ b by Th13, ORDINAL5:51;
consider c being ordinal number such that
A1: epsilon_ (succ a) = 1 -Veblen c by Th14;
A2: a in succ a by ORDINAL1:6;
epsilon_ a in epsilon_ (succ a) by ORDINAL1:6, ORDINAL5:44;
then a in c by Z0, A1, Th15a;
then succ a c= c by ORDINAL1:21;
hence 1 -Veblen (succ a) c= epsilon_ (succ a) by A1, Th15; :: 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 A0, EXCH1;
then b in succ a by LemE2;
then b c= a by ORDINAL1:22;
then epsilon_ b c= epsilon_ a by LemE1;
then succ a c= a by Z0, A0, Th15;
then a in a by A2;
hence contradiction ; :: thesis: verum