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