A1: now

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

end;

now

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

end;

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