per cases ( K is void or not K is void ) ;

suppose K is void ; :: thesis: (degree K) + 1 is natural

then (degree K) + 1 = (- 1) + 1 by Def12
.= 0 ;
hence (degree K) + 1 is natural ; :: thesis: verum

end;

suppose not K is void ; :: thesis: (degree K) + 1 is natural

then consider S being Subset of K such that
A1: S is simplex-like and
A2: card S = (degree K) + 1 by Def12;
( the_family_of K is finite-membered & S in the topology of K ) by A1, MATROID0:def 6;
then S is finite ;
hence (degree K) + 1 is natural by A2; :: thesis: verum

end;

end;