theorem AptIsCoxeterProof.apt_sufficient_foldings {V : Type} [DecidableEq V] (K : ChamberComplex V) (hThick : K.IsThick) (pre : PreApartmentData K) (A : SimplicialComplex V) (hA : A ∈ pre.apartments) : ∃ (cc : ChamberComplex V), cc.toSimplicialComplex = A ∧ cc.IsThin ∧ HasSufficientFoldings cc

Apartments in a thick chamber complex carry a thin chamber-complex structure with sufficient foldings — restatement of the thickness hypothesis specialized to apartments.