theorem PiBase.instQuasiSoberOfSoberSpace {X : Type u} [TopologicalSpace X] [SoberSpace X] : QuasiSober X

Theorem T511: P73 (SoberSpace) => P192 (QuasiSober)

theorem PiBase.Formal.T511 : P73 ≤ P192