instance PiBase.instHasCountableExtentOfHasCountableSpread {X : Type u} [TopologicalSpace X] [h : HasCountableSpread X] : HasCountableExtent X

Theorem T561: P197 (HasCountableSpread) => P198 (HasCountableExtent)

theorem PiBase.Formal.T561 : P197 ≤ P198