A1: now

consider S being T-Sequence such that
A2: ( dom S = A & ( for B being Ordinal st B in A holds
S . B = H₁(B) ) ) from ORDINAL2:sch 2();
assume that
A3: A <> {} and
A4: for B being Ordinal holds A <> succ B ; :: thesis: alef A is Cardinal
A is limit_ordinal by A4, ORDINAL1:29;
then alef A = card (sup S) by A3, A2, Lm1;
hence alef A is Cardinal ; :: thesis: verum

end;

now

given B being Ordinal such that A5: A = succ B ; :: thesis: alef A is cardinal
alef A = nextcard (union {(alef B)}) by A5, Lm1;
hence alef A is cardinal ; :: thesis: verum

end;

hence alef A is cardinal by A1, Lm1; :: thesis: verum