fact: Definition first_order_dedekind := forall Alpha Beta, (forall X, FOF (Alpha X)) -> (forall Y, FOF (Beta Y)) -> (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