instance PiBase.instFirstCountableTopologyOfDevelopableSpace {X : Type u} [TopologicalSpace X] [h : DevelopableSpace X] : FirstCountableTopology X

Theorem T710: P110 (DevelopableSpace) => P28 (FirstCountableTopology)

theorem PiBase.Formal.T710 : P110 ≤ P28