instance PiBase.instPseudoradialSpaceOfRadialSpace {X : Type u} [TopologicalSpace X] [h : RadialSpace X] : PseudoradialSpace X

Theorem T205: P172 (RadialSpace) => P173 (PseudoradialSpace) TODO: Shorten this by using alternative def for PseudoRadial

theorem PiBase.Formal.T205 : P172 ≤ P173