instance PiBase.instSecondCountableTopologyOfIndiscreteTopology {X : Type u} [TopologicalSpace X] [IndiscreteTopology X] : SecondCountableTopology X

Theorem T450: P129 (IndiscreteTopology) => P27 (SecondCountableTopology)

theorem PiBase.Formal.T450 : P129 ≤ P27