for a being Aleph st cf a in a holds
ex xi being Ordinal-Sequence st
( dom xi = cf a & rng xi c= a & xi is increasing & a = sup xi & xi is Cardinal-Function & not 0 in rng xi )