instance PiBase.instHasAnIsolatedPointOfScatteredSpaceOfNonempty {X : Type u} [TopologicalSpace X] [h : ScatteredSpace X] [Nonempty X] : HasAnIsolatedPoint X

Theorem T306: P51 (ScatteredSpace) + ¬P137 (IsEmpty) => P139 (HasAnIsolatedPoint)

theorem PiBase.Formal.T306 : P51 ⊓ P137ᶜ ≤ P139