let a be Aleph; :: thesis: omega c= cf a
A1: a is_cofinal_with cf a by Def1;
then cf a <> {} by ORDINAL2:50;
then A2: {} in cf a by ORDINAL3:8;
cf a is limit_ordinal by A1, ORDINAL4:38;
hence omega c= cf a by A2, ORDINAL1:def 11; :: thesis: verum