theorem PiBase.instCompactlyCoherentSpaceOfCompactlyGeneratedSpace {X : Type u} [TopologicalSpace X] [CompactlyGeneratedSpace X] : CompactlyCoherentSpace X

Theorem T325: P141 (CompactlyGeneratedSpace) => P140 (CompactlyCoherentSpace)

theorem PiBase.Formal.T325 : P141 ≤ P140