theorem section_4_4_corollary_same_system {V : Type} [DecidableEq V] (b : Building V) {L : Type} [DecidableEq L] (𝒜 : ApartmentSystem b.toChamberComplex) (A : SimplicialComplex V) (hA : A ∈ 𝒜.apartments) (A' : SimplicialComplex V) (hA' : A' ∈ 𝒜.apartments) (C : Finset V) (hCmax : A.IsMaximal C) (hCA' : C ∈ A'.faces) (lab : Labelling b.toSimplicialComplex L) : (∃ (φ : SimplicialMap A A'), (∀ (v : V), (∃ s ∈ A.faces, v ∈ s) → (∃ t ∈ A'.faces, v ∈ t) → φ.toFun v = v) ∧ ∀ s ∈ A.faces, lab.labelMap (Finset.image φ.toFun s) = lab.labelMap s) ∧ ∀ (φ : SimplicialMap A A'), Function.Bijective φ.toFun → (∀ (v : V), (∃ s ∈ A.faces, v ∈ s) → (∃ t ∈ A'.faces, v ∈ t) → φ.toFun v = v) → ∀ s ∈ A.faces, lab.labelMap (Finset.image φ.toFun s) = lab.labelMap s

Section 4.4 corollary in the case of a single apartment system $\mathcal{A}$: for apartments $A, A' \in \mathcal{A}$ sharing a chamber $C$ that is maximal in $A$, there exists a label-preserving simplicial map $\varphi : A \to A'$ fixing $A \cap A'$, and every bijective such map preserves labels.