instance PiBase.instK3SpaceOfCompactlyCoherentSpaceOfK1T2Space {X : Type u} [TopologicalSpace X] [h : CompactlyCoherentSpace X] [h' : K1T2Space X] : K3Space X

Theorem T60: P140 (CompactlyCoherentSpace) + P170 (K1T2Space) => P142 (K3Space)

theorem PiBase.Formal.T60 : P140 ⊓ P170 ≤ P142