for A being real-bounded Subset of REAL holds 0 <= xvol A