let p be polyhedron; :: thesis: ( p is simply-connected implies dim (((dim p) - 1) -circuit-space p) = 1 )
assume A1: p is simply-connected ; :: thesis: 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;
((dim p) - 1) -bounding-chain-space p = ((dim p) - 1) -circuit-space p by A1, Th51;
hence dim (((dim p) - 1) -circuit-space p) = 1 by Th79; :: thesis: verum