instance PiBase.instα15SpaceOfα1Space {X : Type u} [TopologicalSpace X] [h : α1Space X] : α15Space X

Theorem T733: P210 (α1Space) => P211 (α15Space)

theorem PiBase.Formal.T733 : P210 ≤ P211