Let X and Tx be given.

Assume Hcomp: compact_space X Tx.

Assume Hman: m_manifold X Tx two.

An exact proof term for the current goal is (compact_manifold_dimension_le X Tx two Hman Hcomp).

∎