theorem :: SIMPLEX0:42

for X being set
for KX being SimplicialComplexStr of X
for i being dim-like number st KX is subset-closed & Skeleton_of (KX,i) is empty-membered & not KX is empty-membered holds
i = - 1