let a be Aleph; :: thesis: omega c= cf a
A1: a is_cofinal_with cf a by Def2;
then cf a <> {} by ORDINAL2:68;
then A2: {} in cf a by ORDINAL3:10;
cf a is limit_ordinal by A1, ORDINAL4:40;
hence omega c= cf a by A2, ORDINAL1:def 12; :: thesis: verum