instance PiBase.instHasCofiniteTopologyOfDiscreteTopologyOfFinite {X : Type u} [TopologicalSpace X] [DiscreteTopology X] [Finite X] : HasCofiniteTopology X

Theorem T782: P52 (DiscreteTopology) + P78 (Finite) => P222 (HasCofiniteTopology)

theorem PiBase.Formal.T782 : P52 ⊓ P78 ≤ P222