let n be Nat; :: thesis: ( cf 0 = 0 & cf (card (n + 1)) = 1 )
A1: succ n is_cofinal_with 1 by ORDINAL3:73;
( card (n + 1) = n + 1 & Segm (n + 1) = succ (Segm n) ) by NAT_1:38;
then cf (card (n + 1)) c= 1 by A1, Def1;
then A2: ( cf (card (n + 1)) = 1 or ( cf (card (n + 1)) = 0 & {} c= n & n in succ n ) ) by ORDINAL1:6, ORDINAL3:16;
( cf 0 c= 0 & 0 c= cf 0 ) by Def1;
hence cf 0 = 0 ; :: thesis: cf (card (n + 1)) = 1
card (n + 1) is_cofinal_with cf (card (n + 1)) by Def1;
hence cf (card (n + 1)) = 1 by A2, ORDINAL2:50; :: thesis: verum