let n be Element of NAT ; :: thesis: ( cf 0 = 0 & cf (card (n + 1)) = 1 )
( 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
A1: ( card (n + 1) = n + 1 & n + 1 = succ n & card (n + 1) is_cofinal_with cf (card (n + 1)) & succ n is_cofinal_with 1 ) by Def2, CARD_1:def 5, NAT_1:39, ORDINAL3:86;
then cf (card (n + 1)) c= 1 by Def2;
then ( 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;
hence cf (card (n + 1)) = 1 by A1, ORDINAL2:68; :: thesis: verum