A1: now :: thesis: ( A <> {} & ( for B being Ordinal holds A <> succ B ) implies aleph A is Cardinal )
consider S being Sequence such that
A2: ( dom S = A & ( for B being Ordinal st B in A holds
S . B = H1(B) ) ) from ORDINAL2:sch 2();
assume that
A3: A <> {} and
A4: for B being Ordinal holds A <> succ B ; :: thesis: aleph A is Cardinal
aleph A = card (sup S) by A3, A2, Lm1, A4, ORDINAL1:29;
hence aleph A is Cardinal ; :: thesis: verum
end;
now :: thesis: ( ex B being Ordinal st A = succ B implies aleph A is cardinal )
given B being Ordinal such that A5: A = succ B ; :: thesis: aleph A is cardinal
aleph A = nextcard (aleph B) by A5, Lm1;
hence aleph A is cardinal ; :: thesis: verum
end;
hence aleph A is cardinal by A1, Lm1; :: thesis: verum