✐‹creator "Kevin Kappelmann"› theory Order_Functions imports Order_Functions_Base Closure_Operators begin paragraph ‹Summary› text ‹Basic functions on orders.› end