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 S1[ polyhedron] means for n being Integer holds n -circuit-space $1 = n -bounding-chain-space $1;
thus ( p is simply-connected implies S1[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: S1[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 ( S1[p] implies p is simply-connected ) ; :: thesis: verum