instance PiBase.instBasicallyDisconnectedSpaceOfExtremallyDisconnected {X : Type u} [TopologicalSpace X] [h : ExtremallyDisconnected X] : BasicallyDisconnectedSpace X

Theorem T693: P49 (ExtremallyDisconnected) => P85 (BasicallyDisconnectedSpace)

theorem PiBase.Formal.T693 : P49 ≤ P85