theorem PiBase.instSequentialSpaceOfFrechetUrysohnSpace {X : Type u} [TopologicalSpace X] [FrechetUrysohnSpace X] : SequentialSpace X

Theorem T184: P80 (FrechetUrysohnSpace) => P79 (SequentialSpace)

theorem PiBase.Formal.T184 : P80 ≤ P79