let a be Ordinal; :: thesis:
let U be Universe; :: thesis:
assume A1: omega in U ; :: thesis:
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]

let b be Ordinal; :: thesis:
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:

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]

let b be Ordinal; :: thesis:
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:

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

end;

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

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: