theorem PiBase.instSequentialSpaceOfWeaklyFirstCountableSpace {X : Type u} [TopologicalSpace X] [hX : WeaklyFirstCountableSpace X] : SequentialSpace X

Theorem T840: P228 (WeaklyFirstCountableSpace) => P79 (SequentialSpace)

theorem PiBase.Formal.T840 : P228 ≤ P79