:: deftheorem Def15 defines -Veblen ORDINAL6:def 15 :
for U being Universe
for b₂ being Ordinal-Sequence-valued Sequence holds
( b₂ = U -Veblen iff ( dom b₂ = On U & b₂ . 0 = U exp omega & ( for b being Ordinal st succ b in On U holds
b₂ . (succ b) = criticals (b₂ . b) ) & ( for l being limit_ordinal non empty Ordinal st l in On U holds
b₂ . l = criticals (b₂ | l) ) ) );