let p be polyhedron; :: thesis: ( p is simply-connected iff for n being Integer holds n -circuit-space p = n -bounding-chain-space p )
defpred S₁[ polyhedron] means for n being Integer holds n -circuit-space $1 = n -bounding-chain-space $1;
thus ( p is simply-connected implies S₁[p] ) :: thesis: ( ( for n being Integer holds n -circuit-space p = n -bounding-chain-space p ) implies p is simply-connected )

proof

assume A1: p is simply-connected ; :: thesis: S₁[p]
let n be Integer; :: thesis: n -circuit-space p = n -bounding-chain-space p
n -circuits p = n -bounding-chains p by A1;
hence n -circuit-space p = n -bounding-chain-space p by VECTSP_4:29; :: thesis: verum

end;

thus ( S₁[p] implies p is simply-connected ) ; :: thesis: verum