environ
vocabularies HIDDEN, NUMBERS, SUBSET_1, ORDINAL1, CARD_1, FUNCT_1, ORDINAL2, TARSKI, CARD_3, RELAT_1, FINSET_1, XBOOLE_0, ARYTM_3, WELLORD1, WELLORD2, ORDINAL4, CARD_2, ORDINAL3, ZFMISC_1, FUNCT_2, FUNCOP_1, MCART_1, CARD_5, MEMBERED, NAT_1;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, CARD_1, ORDINAL1, NUMBERS, XCMPLX_0, NAT_1, MEMBERED, RELAT_1, FUNCT_1, FINSET_1, FUNCT_2, WELLORD1, WELLORD2, XTUPLE_0, MCART_1, FUNCOP_1, ORDINAL2, ORDINAL3, CARD_2, CARD_3, ORDINAL4;
definitions TARSKI, FUNCT_1, ORDINAL2, CARD_1, CARD_3, XBOOLE_0, ORDINAL1;
theorems TARSKI, FUNCT_1, FUNCT_2, FUNCOP_1, NAT_1, FINSET_1, ORDINAL1, ORDINAL2, ORDINAL3, ORDINAL4, WELLORD1, WELLORD2, CARD_1, CARD_2, CARD_3, CARD_4, ZFMISC_1, FUNCT_4, FUNCT_5, RELAT_1, XBOOLE_0, XBOOLE_1, XTUPLE_0;
schemes FUNCT_1, ORDINAL1, PARTFUN1, CARD_1, CARD_3, ORDINAL2, CLASSES1, XBOOLE_0, CARD_2, XFAMILY;
registrations XBOOLE_0, FUNCT_1, ORDINAL1, FUNCOP_1, ORDINAL2, ORDINAL3, NAT_1, CARD_1, CARD_3, ORDINAL4, MEMBERED, FINSET_1, CARD_2, XTUPLE_0, XCMPLX_0;
constructors HIDDEN, WELLORD1, WELLORD2, FUNCOP_1, ORDINAL3, XXREAL_0, NAT_1, FINSEQ_1, CARD_2, CARD_3, ORDINAL4, RELSET_1, MEMBERED, ORDERS_1, XREAL_0, XTUPLE_0, NUMBERS;
requirements HIDDEN, NUMERALS, REAL, BOOLE, SUBSET, ARITHM;
equalities ORDINAL2, CARD_3, ORDINAL1, CARD_1;
expansions TARSKI, FUNCT_1, ORDINAL2, CARD_1, XBOOLE_0;
Lm1:
1 = card 1
;
Lm2:
2 = card 2
;
Lm3:
for phi, psi being Ordinal-Sequence st rng phi = rng psi & phi is increasing & psi is increasing holds
for A being Ordinal st A in dom phi holds
( A in dom psi & phi . A = psi . A )
Lm4:
for O being Ordinal
for X being finite set st X c= O holds
order_type_of (RelIncl X) is finite