let M be Aleph; :: thesis: for X being Subset of M st X is unbounded holds
cf M c= card X
let X be Subset of M; :: thesis: ( X is unbounded implies cf M c= card X )
assume A1: X is unbounded ; :: thesis: cf M c= card X
assume not cf M c= card X ; :: thesis: contradiction
then card X in cf M by ORDINAL1:26;
then A2: sup X in M by CARD_5:38;
sup X = M by A1, Def4;
hence contradiction by A2; :: thesis: verum