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

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