let K be SimplicialComplexStr; :: thesis: - 1 <= degree K

per cases ( K is void or ( not K is void & K is finite-degree ) or ( not K is void & not K is finite-degree ) ) ;

suppose K is void ; :: thesis: - 1 <= degree K

hence - 1 <= degree K by Def12; :: thesis: verum

end;

suppose A1: ( not K is void & K is finite-degree ) ; :: thesis: - 1 <= degree K

then reconsider d = degree K as Integer ;
( 0 = (- 1) + 1 & d + 1 >= 0 ) by A1;
hence - 1 <= degree K by XREAL_1:6; :: thesis: verum

end;

suppose ( not K is void & not K is finite-degree ) ; :: thesis: - 1 <= degree K

hence - 1 <= degree K by Def12; :: thesis: verum

end;

end;