fact: Definition dedekind_s_axiom := forall (Alpha Beta : Tpoint -> Prop), (exists A, forall X Y, Alpha X -> Beta Y -> Bet A X Y) -> (exists B, forall X Y, Alpha X -> Beta Y -> Bet X B Y).
imports: GeoCoq.Tarski_dev.Definitions