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

Theorem T736: P213 (α3Space) => P214 (α4Space)

theorem PiBase.Formal.T736 : P213 ≤ P214