instance PiBase.instT1SpaceOfHasCofiniteTopology {X : Type u} [TopologicalSpace X] [h : HasCofiniteTopology X] : T1Space X

Theorem T779: P222 (HasCofiniteTopology) => P2 (T1Space)

theorem PiBase.Formal.T779 : P222 ≤ P2