environ
vocabularies HIDDEN, XBOOLE_0, ORDINAL1, ZF_LANG, SUBSET_1, NUMBERS, ZF_MODEL, TARSKI, FUNCT_1, REALSET1, CARD_1, CLASSES2, ZF_REFLE, ORDINAL2, ARYTM_3, BVFUNC_2, RELAT_1, ZFMISC_1, FUNCT_2, ORDINAL4, FUNCT_5, CARD_3, CLASSES1, ZFREFLE1, NAT_1;
notations HIDDEN, TARSKI, XBOOLE_0, ENUMSET1, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, FUNCT_2, BINOP_1, CARD_1, ORDINAL1, XCMPLX_0, NAT_1, ZF_LANG, ZF_MODEL, ORDINAL2, NUMBERS, CARD_3, FUNCT_5, ORDINAL3, CLASSES1, CLASSES2, ORDINAL4, ZF_LANG1, ZF_REFLE;
definitions TARSKI, ORDINAL2, ZF_MODEL, ORDINAL1, XBOOLE_0;
theorems TARSKI, ZFMISC_1, FUNCT_1, FUNCT_2, FUNCT_5, ORDINAL1, ORDINAL2, ORDINAL3, ORDINAL4, CARD_1, CARD_2, CLASSES1, CLASSES2, ZF_LANG, CARD_3, ZF_MODEL, ZFMODEL1, ZF_LANG1, ZF_REFLE, RELAT_1, RELSET_1, XBOOLE_0, XBOOLE_1, XCMPLX_1;
schemes NAT_1, ORDINAL2, ORDINAL4, ZF_REFLE, FUNCT_1, XBOOLE_0;
registrations XBOOLE_0, SUBSET_1, ORDINAL1, RELSET_1, ORDINAL2, XREAL_0, CARD_1, CLASSES2, ZF_LANG, ZF_LANG1, CLASSES1, ORDINAL4, FUNCT_1, NAT_1;
constructors HIDDEN, ENUMSET1, WELLORD2, BINOP_1, ORDINAL3, XXREAL_0, XREAL_0, NAT_1, FUNCT_5, CLASSES1, ZF_MODEL, ZF_LANG1, ZF_REFLE, ORDINAL4, RELSET_1, NUMBERS;
requirements HIDDEN, NUMERALS, BOOLE, SUBSET;
equalities ORDINAL2, ORDINAL1, BINOP_1, ORDINAL4;
expansions TARSKI, ORDINAL2, XBOOLE_0;
Lm1:
{} in omega
by ORDINAL1:def 11;
Lm2:
omega is limit_ordinal
by ORDINAL1:def 11;
defpred S1[ object ] means ( $1 = the_axiom_of_extensionality or $1 = the_axiom_of_pairs or $1 = the_axiom_of_unions or $1 = the_axiom_of_infinity or $1 = the_axiom_of_power_sets or ex H being ZF-formula st
( {(x. 0),(x. 1),(x. 2)} misses Free H & $1 = the_axiom_of_substitution_for H ) );