instance PiBase.instHomogeneousSpaceOfDiscreteTopology {X : Type u} [TopologicalSpace X] [h : DiscreteTopology X] : HomogeneousSpace X

Theorem T204: P52 (DiscreteTopology) => P86 (HomogeneousSpace) Note the use of classical

theorem PiBase.Formal.T204 : P52 ≤ P86