proposition: Lemma continuity : continuityP Point Bet.
proof: Proof. unfold continuityP, Bet; intros Xi Upsilon [A H]; exists A; intros X Y HX HY. assert (HBet := H _ _ HX HY); destruct A, X, Y; tauto. Qed.
imports: GeoCoq.Meta_theory.Counter_models.Planar.independence