begin
:: deftheorem Def1 defines cardinal CARD_1:def 1 :
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem Th4:
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem Th8:
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
theorem
:: deftheorem CARD_1:def 2 :
canceled;
:: deftheorem CARD_1:def 3 :
canceled;
:: deftheorem CARD_1:def 4 :
canceled;
:: deftheorem Def5 defines card CARD_1:def 5 :
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem Th21:
theorem Th22:
theorem Th23:
theorem Th24:
theorem
theorem Th26:
theorem Th27:
theorem
theorem Th29:
theorem Th30:
:: deftheorem Def6 defines nextcard CARD_1:def 6 :
theorem
canceled;
theorem Th32:
theorem
theorem Th34:
theorem Th35:
theorem
:: deftheorem Def7 defines limit_cardinal CARD_1:def 7 :
:: deftheorem Def8 defines alef CARD_1:def 8 :
deffunc H1( Ordinal) -> set = alef $1;
theorem
canceled;
theorem
canceled;
theorem Th39:
theorem
theorem Th41:
theorem Th42:
theorem
theorem
theorem
theorem Th46:
theorem
theorem Th48:
theorem
theorem
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem Th58:
theorem Th59:
theorem Th60:
theorem Th61:
theorem Th62:
theorem Th63:
theorem
canceled;
Lm2:
for n, m being natural number st n,m are_equipotent holds
n = m
theorem Th65:
theorem
canceled;
theorem
canceled;
theorem Th68:
theorem Th69:
theorem
canceled;
theorem
theorem
theorem Th73:
theorem Th74:
theorem
canceled;
theorem Th76:
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
scheme
CardinalCompInd{
P1[
set ] } :
provided
theorem Th83:
theorem
theorem
canceled;
theorem
Lm3:
for A being Ordinal
for n being natural number st A,n are_equipotent holds
A = n
Lm4:
for A being Ordinal holds
( A is finite iff A in omega )
begin
theorem Th87:
theorem Th88:
theorem Th89:
theorem Th90:
theorem Th91:
theorem Th92:
theorem Th93:
theorem Th94:
theorem Th95:
theorem
10
= {0 ,1,2,3,4,5,6,7,8,9}
theorem
:: deftheorem CARD_1:def 9 :
canceled;
:: deftheorem CARD_1:def 10 :
canceled;
:: deftheorem CARD_1:def 11 :
canceled;
:: deftheorem defines Segm CARD_1:def 12 :
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
theorem
theorem