theorem :: POLYFORM:49

for p being polyhedron
for k being Integer holds dim (k -chain-space p) = (rank (k -boundary p)) + (nullity (k -boundary p)) by RANKNULL:44;