environ
vocabularies HIDDEN, ORDINAL6, CARD_1, RELAT_1, FUNCT_1, CLASSES2, NUMBERS, TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, ORDINAL2, WELLORD1, WELLORD2, ABIAN, CARD_3, MATROID0, ORDINAL4, NAT_1, ARYTM_3, CLASSES1, VALUED_0, AFINSQ_1, ORDINAL5, ZFMISC_1, FINSET_1, MESFUNC8, NAGATA_1, ORDINAL3, PRE_TOPC, AOFA_000;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, PARTFUN1, FUNCT_2, FINSET_1, ORDINAL1, ORDINAL2, XCMPLX_0, NAT_1, ORDINAL3, ABIAN, WELLORD1, WELLORD2, CARD_1, ORDINAL4, CARD_3, AFINSQ_1, CLASSES1, CLASSES2, NUMBERS, ORDINAL5;
definitions TARSKI, XBOOLE_0, FUNCT_1, WELLORD1, ABIAN, ORDINAL1, ORDINAL2, CARD_3, ORDINAL5;
theorems XBOOLE_1, ZFMISC_1, RELAT_1, FUNCT_1, ORDINAL1, ORDINAL2, ORDINAL3, FUNCT_3, WELLORD1, WELLORD2, ORDERS_1, CARD_2, CARD_5, FUNCT_2, ORDINAL4, XBOOLE_0, TARSKI, ORDINAL5, NAT_1, CLASSES1, CLASSES2, CARD_1, AFINSQ_1, NAT_2, GRFUNC_1;
schemes NAT_1, ORDINAL1, ORDINAL2, ORDINAL4, TREES_2;
registrations XBOOLE_0, RELAT_1, RELSET_1, FUNCT_1, FINSET_1, FUNCT_2, ORDINAL1, ORDINAL2, CARD_1, WELLORD2, ORDINAL3, CLASSES2, CARD_5, ORDINAL4, CARD_LAR, ORDINAL5, CLASSES1, AFINSQ_1, SUBSET_1, XCMPLX_0, NAT_1;
constructors HIDDEN, WELLORD1, WELLORD2, CLASSES1, ABIAN, CARD_3, AFINSQ_1, ORDINAL3, ORDINAL5, NAT_1, RELSET_1, NUMBERS;
requirements HIDDEN, SUBSET, BOOLE, NUMERALS;
equalities ORDINAL1, ORDINAL2, ORDINAL4, CARD_3, CARD_1;
expansions TARSKI, XBOOLE_0, FUNCT_1, WELLORD1, ABIAN, ORDINAL1, ORDINAL2, ORDINAL5;
Lm1:
for U being Universe st omega in U holds
(U -Veblen) . 0 is normal Ordinal-Sequence of U
Lm2:
for a being Ordinal
for U being Universe st omega in U & a in U & (U -Veblen) . a is normal Ordinal-Sequence of U holds
(U -Veblen) . (succ a) is normal Ordinal-Sequence of U
Lm3:
for l being limit_ordinal non empty Ordinal
for U being Universe st l in U & ( for a being Ordinal st a in l holds
(U -Veblen) . a is normal Ordinal-Sequence of U ) holds
(U -Veblen) . l is normal Ordinal-Sequence of U
Lm4:
1 -Veblen 0 = epsilon_ 0
Lm5:
for a being Ordinal st 1 -Veblen a = epsilon_ a holds
1 -Veblen (succ a) = epsilon_ (succ a)
Lm6:
for l being limit_ordinal non empty Ordinal st ( for a being Ordinal st a in l holds
1 -Veblen a = epsilon_ a ) holds
1 -Veblen l = epsilon_ l