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 X is unbounded ; :: thesis: cf M c= card X
then A1: sup X = M ;
assume not cf M c= card X ; :: thesis: contradiction
then card X in cf M by ORDINAL1:16;
then sup X in M by CARD_5:26;
hence contradiction by A1; :: thesis: verum