let p be polyhedron; :: thesis: ( p is simply-connected implies dim (((dim p) - 1) -circuit-space p) = 1 )
set d = dim p;
set U = ((dim p) - 1) -bounding-chain-space p;
set V = ((dim p) - 1) -circuit-space p;
assume p is simply-connected ; :: thesis: dim (((dim p) - 1) -circuit-space p) = 1
then ((dim p) - 1) -bounding-chain-space p = ((dim p) - 1) -circuit-space p by Th48;
hence dim (((dim p) - 1) -circuit-space p) = 1 by Th76; :: thesis: verum