The weak-join model is a CW K(G,1)

Each simplex is a closed finite-dimensional disk with its usual faces, attached to the previously constructed skeleton. Its boundary has finitely many faces. The finite-boundary-support CW construction gives J(G) and its weak topology, with disjoint simplex interiors. The action preserves faces and their slot ordering, and is free: any occupied slot has label g, and gh=g forces h=1. Distinct vertices of a simplex have different slots, so no nonidentity action identifies two points within one simplex. For B_wG choose one representative for each orbit of simplices, oriented in increasing slot order. Their disks attach by their face orbits, with finite boundary support and disjoint interiors. A set is closed in this cell construction exactly when its inverse image is closed on each simplex of J(G); that is also the orbit-quotient closed-set criterion. Thus the constructed CW topology is exactly the orbit topology.

Let t_s be the weight in slot s. It is continuous by the map-out criterion on each characteristic simplex. On its positive locus the label g_s is continuous into discrete G: the open star of (s,g) is the locus t_s>0, g_s=g, checked on each simplex. Let U_s⊂B_wG be t_s>0. Normalizing a representative by right multiplication by g_s^{-1} defines a section on U_s, since (x h)(g_s h)^{-1}=x g_s^{-1}. On the corresponding open sets the normalizing map is continuous, as is seen on every characteristic simplex with its fixed slot labels. Its descended section is continuous by the quotient criterion restricted to the saturated open preimage. The maps (b,h)↦s_s(b)h and x↦(p(x),g_s(x)) are continuous inverses between U_s×G and p^{-1}U_s. These are ordinary covering charts because G is discrete. The charts cover B_wG.

Any two vertices of J(G) are joined by an edge if their slots differ; otherwise insert a vertex in a different slot and use two edges. Every point lies in a simplex and joins a vertex there, so J(G) is path-connected. A sphere map into J(G) meets finitely many cells by the published compact CW-support lemma. These cells use finitely many slots. Select another slot and the vertex labelled 1 in it. Coning each of those finitely many simplices to this vertex gives a finite subcomplex, and the barycentric join homotopy contracts the image inside it. The finite disk/face formulas agree and give an ordinary continuous homotopy. Thus all positive homotopy groups vanish. An unbased contraction of one sphere map also makes its based class zero: basepoint transport along the homotopy track is an isomorphism and carries it to the constant class. This uses no global contraction or unproved compact-stage assertion.

The covering is a fibration by the published covering-lifting lemma. Fix the vertex $(0,1_G)$ upstairs and its image downstairs. Lifting a loop gives a unique endpoint $(0,g)$; the marking is $[\alpha ]\mapsto g^{-1}$. For successive loops with endpoints $a$ and $b$, the second lift starting at $(0,a)$ is the right translate by $a$ of its lift from $(0,1_G)$, so the concatenated endpoint is $ba$. Taking inverses makes the marking a homomorphism for left-to-right loop concatenation. It is surjective because the total space is path connected; its kernel is zero because a closed lifted loop is nullhomotopic in the simply connected total space and its nullhomotopy projects downstairs. The fibration exact sequence and the discrete fiber give ${\pi }_i(B_{w}G)=0$ for $i>1$. Hence this is the stated marked CW $K(G,1)$.

For H≤G, an orbit of a simplex whose labels lie in H can coincide with another such orbit under a translation g∈G only when g∈H: inspecting one vertex proves this. Therefore the H-orbit cells inject, and their faces remain H-orbit cells, giving a subcomplex B_wH. Normalize each simplex orbit by making its first label 1. Its remaining finitely many labels generate a finitely generated subgroup. Taking generators from finitely many cells gives one subgroup containing all those cells and their faces. This proves the final assertion.