DEFINITION MODULE RealBox = OrdBox(REAL);
END RealBox.