environ
vocabularies HIDDEN, ORDINAL1, RELAT_1, FUNCT_1, XBOOLE_0, TARSKI, WELLORD1, WELLORD2, ZFMISC_1, ORDINAL2, FUNCOP_1, FINSET_1, SUBSET_1, MCART_1, CARD_1, BSPACE, NAT_1, XCMPLX_0, FUNCT_4, QUANTAL1;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, ENUMSET1, XTUPLE_0, MCART_1, FUNCT_1, FUNCOP_1, WELLORD1, ORDINAL1, ORDINAL2, WELLORD2, FINSET_1, FUNCT_4;
definitions ORDINAL1, TARSKI, FUNCT_1, FINSET_1, WELLORD2, XBOOLE_0, RELAT_1;
theorems TARSKI, FUNCT_1, ZFMISC_1, ORDINAL1, ORDINAL2, WELLORD1, WELLORD2, RELAT_1, FINSET_1, XBOOLE_0, XBOOLE_1, FUNCOP_1, ENUMSET1, ORDINAL3, MCART_1, XTUPLE_0, FUNCT_4;
schemes ORDINAL1, ORDINAL2, FUNCT_1, FINSET_1, XBOOLE_0, PARTFUN1;
registrations XBOOLE_0, SUBSET_1, FUNCT_1, ORDINAL1, FUNCOP_1, FINSET_1, ZFMISC_1, XTUPLE_0, FUNCT_4;
constructors HIDDEN, ENUMSET1, WELLORD1, WELLORD2, FUNCOP_1, ORDINAL2, FINSET_1, XTUPLE_0, FUNCT_4;
requirements HIDDEN, NUMERALS, SUBSET, BOOLE;
equalities ORDINAL1, RELAT_1;
expansions ORDINAL1, TARSKI, FUNCT_1, FINSET_1, WELLORD2, XBOOLE_0;
deffunc H1( Ordinal) -> set = aleph $1;
Lm2:
for m, n being Nat st n,m are_equipotent holds
n = m
Lm3:
for X being set st X is finite holds
ex n being Nat st X,n are_equipotent
scheme
CardinalCompInd{
P1[
set ] } :
provided
Lm4:
for A being Ordinal
for n being Nat st A,n are_equipotent holds
A = n
Lm5:
for A being Ordinal holds
( A is finite iff A in omega )
theorem
10
= {0,1,2,3,4,5,6,7,8,9}
canceled;