theorem PiBase.instQuasiSoberOfR1Space {X : Type u} [TopologicalSpace X] [R1Space X] : QuasiSober X

Theorem T519: P134 (R1Space) => P192 (QuasiSober)

theorem PiBase.Formal.T519 : P134 ≤ P192