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

Theorem T735: P212 (α2Space) => P213 (α3Space)

theorem PiBase.Formal.T735 : P212 ≤ P213