theorem :: CARD_1:20

for A being Ordinal st A <> {} & A is limit_ordinal holds
for S being Sequence st dom S = A & ( for B being Ordinal st B in A holds
S . B = aleph B ) holds
aleph A = card (sup S) by Lm1;