theorem :: INTEGRA1:9

for A being non empty real-bounded Subset of REAL holds 0 <= vol A by SEQ_4:11, XREAL_1:48;