let a be ordinal number ; :: 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 Z0: 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 );
00: S₁[ 0 ] by Z0, Th21;
01: for b being ordinal number st S₁[b] holds
S₁[ succ b]

proof

let b be ordinal number ; :: 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 Z0, Th22; :: thesis: verum

end;

02: for b being ordinal number st b <> {} & b is limit_ordinal & ( for c being ordinal number st c in b holds
S₁[c] ) holds
S₁[b]

proof

let b be ordinal number ; :: thesis: ( b <> {} & b is limit_ordinal & ( for c being ordinal number st c in b holds
S₁[c] ) implies S₁[b] )
assume that
A1: ( b <> {} & b is limit_ordinal ) and
A2: for c being ordinal number st c in b holds
S₁[c] and
A3: b in U ; :: thesis: (U -Veblen) . b is normal Ordinal-Sequence of U

now

let a be ordinal number ; :: thesis: ( a in b implies (U -Veblen) . a is normal Ordinal-Sequence of U )
assume A4: a in b ; :: thesis: (U -Veblen) . a is normal Ordinal-Sequence of U
then a in U by A3, ORDINAL1:10;
hence (U -Veblen) . a is normal Ordinal-Sequence of U by A2, A4; :: thesis: verum

end;

hence (U -Veblen) . b is normal Ordinal-Sequence of U by A1, A3, Th61; :: thesis: verum

end;

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