let U be Universe; :: thesis: ( omega in U implies (U -Veblen) . 0 is normal Ordinal-Sequence of U )
assume omega in U ; :: thesis: (U -Veblen) . 0 is normal Ordinal-Sequence of U
then reconsider o = omega as non trivial Ordinal of U ;
(U -Veblen) . 0 = U exp o by Def15;
hence (U -Veblen) . 0 is normal Ordinal-Sequence of U ; :: thesis: verum