let K be SimplicialComplexStr; :: thesis: ( degree K = - 1 iff K is empty-membered )

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

suppose K is void ; :: thesis: ( degree K = - 1 iff K is empty-membered )

hence ( degree K = - 1 iff K is empty-membered ) by Def12; :: thesis: verum

end;

suppose A1: not K is void ; :: thesis: ( degree K = - 1 iff K is empty-membered )

hereby :: thesis: ( K is empty-membered implies degree K = - 1 )

assume A2: degree K = - 1 ; :: thesis: not K is with_non-empty_element
then A3: K is finite-degree by A1, Def12;
assume K is with_non-empty_element ; :: thesis: contradiction
then the topology of K is with_non-empty_element ;
then consider S being non empty set such that
A4: S in the topology of K ;
reconsider S = S as Subset of K by A4;
A5: S is simplex-like by A4;
then reconsider S = S as finite Subset of K by A1, A3;
card S <= (- 1) + 1 by A1, A2, A3, A5, Def12;
then card S = 0 ;
hence contradiction ; :: thesis: verum

end;

assume A6: K is empty-membered ; :: thesis: degree K = - 1
then consider S being Subset of K such that
A7: S is simplex-like and
A8: card S = (degree K) + 1 by A1, Def12;
A9: S in the topology of K by A7;
assume degree K <> - 1 ; :: thesis: contradiction
then card S <> (- 1) + 1 by A8, XXREAL_3:11;
then A10: not S is empty ;
the topology of K is empty-membered by A6;
hence contradiction by A9, A10; :: thesis: verum

end;

end;