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;