instance PiBase.instCardGeThreeOfHasACutPoint {X : Type u} [TopologicalSpace X] [h : HasACutPoint X] : CardGeThree X

Theorem T558: P204 (HasACutPoint) => P175 (CardGeThree)

theorem PiBase.Formal.T558 : P204 ≤ P175