begin
Lm1:
1 = card 1
by CARD_1:def 5;
Lm2:
2 = card 2
by CARD_1:def 5;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
begin
theorem Th9:
theorem Th10:
theorem Th11:
theorem Th12:
theorem
canceled;
theorem Th14:
theorem Th15:
theorem Th16:
theorem Th17:
theorem Th18:
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 )
theorem
theorem Th20:
theorem Th21:
theorem
theorem Th23:
:: deftheorem CARD_5:def 1 :
canceled;
:: deftheorem Def2 defines cf CARD_5:def 2 :
for M, b2 being Cardinal holds
( b2 = cf M iff ( M is_cofinal_with b2 & ( for N being Cardinal st M is_cofinal_with N holds
b2 c= N ) ) );
:: deftheorem Def3 defines -powerfunc_of CARD_5:def 3 :
for M, N being Cardinal
for b3 being Cardinal-Function holds
( b3 = N -powerfunc_of M iff ( ( for x being set holds
( x in dom b3 iff ( x in M & x is Cardinal ) ) ) & ( for K being Cardinal st K in M holds
b3 . K = exp K,N ) ) );
begin
theorem
theorem Th25:
theorem Th26:
theorem Th27:
theorem
theorem
canceled;
theorem
canceled;
theorem Th31:
theorem
begin
:: deftheorem defines regular CARD_5:def 4 :
for IT being Aleph holds
( IT is regular iff cf IT = IT );
theorem
canceled;
theorem Th34:
Lm4:
1 = card 1
by CARD_1:def 5;
theorem Th35:
theorem Th36:
theorem
theorem Th38:
theorem Th39:
theorem Th40:
theorem Th41:
theorem
begin
theorem Th43:
theorem
theorem Th45:
theorem
theorem
Lm1:
for O being Ordinal
for X being finite set st X c= O holds
order_type_of (RelIncl X) is finite
theorem Th48:
theorem Th49:
theorem
theorem