Let X, Tx and n be given.
Assume HTx: topology_on X Tx.
Assume Hn: n ∈ ω.
Assume Hprop: ∀A : set, open_cover_of X Tx A → ∃B : set, open_cover_of X Tx B ∧ refines_cover B A ∧ collection_has_order_at_most_m_plus_one X B n.
We will prove covering_dimension X Tx n.
An exact proof term for the current goal is (andI (topology_on X Tx ∧ n ∈ ω) (∀A : set, open_cover_of X Tx A → ∃B : set, open_cover_of X Tx B ∧ refines_cover B A ∧ collection_has_order_at_most_m_plus_one X B n) (andI (topology_on X Tx) (n ∈ ω) HTx Hn) Hprop).
∎