fact: Definition algebraic_dcpo_struct_to_continuous {X : dcpo} (AX : algebraic_dcpo_struct X) : continuous_dcpo_struct X.
imports: UniMath.MoreFoundations.All UniMath.OrderTheory.DCPOs.Core.DirectedSets UniMath.OrderTheory.DCPOs.Core.Basics UniMath.OrderTheory.DCPOs.Core.WayBelow UniMath.OrderTheory.DCPOs.Basis.Continuous