let a be Ordinal; :: thesis: for U being Universe st omega in U & a in U holds
(U -Veblen) . a is normal Ordinal-Sequence of U
let U be Universe; :: thesis: ( omega in U & a in U implies (U -Veblen) . a is normal Ordinal-Sequence of U )
assume A1: omega in U ; :: thesis: ( not a in U or (U -Veblen) . a is normal Ordinal-Sequence of U )
defpred S₁[ Ordinal] means ( $1 in U implies (U -Veblen) . $1 is normal Ordinal-Sequence of U );
A2: S₁[ 0 ] by A1, Lm1;
A3: for b being Ordinal st S₁[b] holds
S₁[ succ b]

proof

let b be Ordinal; :: thesis: ( S₁[b] implies S₁[ succ b] )
b in succ b by ORDINAL1:6;
then ( succ b in U implies b in U ) by ORDINAL1:10;
hence ( S₁[b] implies S₁[ succ b] ) by A1, Lm2; :: thesis: verum

end;

A4: for b being Ordinal st b <> 0 & b is limit_ordinal & ( for c being Ordinal st c in b holds
S₁[c] ) holds
S₁[b]

proof

let b be Ordinal; :: thesis: ( b <> 0 & b is limit_ordinal & ( for c being Ordinal st c in b holds
S₁[c] ) implies S₁[b] )
assume that
A5: ( b <> 0 & b is limit_ordinal ) and
A6: for c being Ordinal st c in b holds
S₁[c] and
A7: b in U ; :: thesis: (U -Veblen) . b is normal Ordinal-Sequence of U

now :: thesis: for a being Ordinal st a in b holds
(U -Veblen) . a is normal Ordinal-Sequence of U

let a be Ordinal; :: thesis: ( a in b implies (U -Veblen) . a is normal Ordinal-Sequence of U )
assume A8: a in b ; :: thesis: (U -Veblen) . a is normal Ordinal-Sequence of U
then a in U by A7, ORDINAL1:10;
hence (U -Veblen) . a is normal Ordinal-Sequence of U by A6, A8; :: thesis: verum

end;

hence (U -Veblen) . b is normal Ordinal-Sequence of U by A5, A7, Lm3; :: thesis: verum

end;

for b being Ordinal holds S₁[b] from ORDINAL2:sch 1(A2, A3, A4);
hence ( not a in U or (U -Veblen) . a is normal Ordinal-Sequence of U ) ; :: thesis: verum