theorem PiBase.instCompactlyGeneratedSpaceOfSequentialSpace {X : Type u} [TopologicalSpace X] [SequentialSpace X] : CompactlyGeneratedSpace X

Theorem T59: P79 (SequentialSpace) => P141 (CompactlyGeneratedSpace)

theorem PiBase.Formal.T59 : P79 ≤ P141