let i be Integer; :: thesis: for K being non void subset-closed SimplicialComplexStr
for S being Simplex of i,K st not S is empty holds
i is natural
let K be non void subset-closed SimplicialComplexStr; :: thesis: for S being Simplex of i,K st not S is empty holds
i is natural
let S be Simplex of i,K; :: thesis: ( not S is empty implies i is natural )
assume not S is empty ; :: thesis: i is natural
then ( - 1 <= i & i <> - 1 ) by Def18;
then - 1 < i by XXREAL_0:1;
then i >= 0 by INT_1:21;
then i in NAT by INT_1:16;
hence i is natural ; :: thesis: verum