let n be Element of NAT ; :: thesis: ( cf 0 = 0 & cf (card (n + 1)) = 1 )
A1: succ n is_cofinal_with 1 by ORDINAL3:86;
( card (n + 1) = n + 1 & n + 1 = succ n ) by CARD_1:def 5, NAT_1:39;
then cf (card (n + 1)) c= 1 by A1, Def2;
then A2: ( cf (card (n + 1)) = 1 or ( cf (card (n + 1)) = 0 & {} c= n & n in succ n ) ) by ORDINAL1:10, ORDINAL3:19, XBOOLE_1:2;
( cf 0 c= 0 & 0 c= cf 0 ) by Def2, XBOOLE_1:2;
hence cf 0 = 0 by XBOOLE_0:def 10; :: thesis: cf (card (n + 1)) = 1
card (n + 1) is_cofinal_with cf (card (n + 1)) by Def2;
hence cf (card (n + 1)) = 1 by A2, ORDINAL2:68; :: thesis: verum