theorem PiBase.instT35SpaceOfCechCompleteSpace {X : Type u} [TopologicalSpace X] [CechCompleteSpace X] : T35Space X

Theorem T610: P63 (CechCompleteSpace) => P6 (T35Space)

theorem PiBase.Formal.T610 : P63 ≤ P6