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: K is empty-membered
then A3: K is finite-degree by A1, Def12;
assume not K is empty-membered ; :: thesis: contradiction
then not the topology of K is empty-membered by Def7;
then consider S being non empty set such that
A4: S in the topology of K by SETFAM_1:def 10;
reconsider S = S as Subset of K by A4;
A5: S is simplex-like by A4, PRE_TOPC:def 2;
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, PRE_TOPC:def 2;
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, Def7;
hence contradiction by A9, A10, SETFAM_1:def 10; :: thesis: verum

end;

end;