let A be real-bounded Subset of REAL; :: thesis: 0 <= xvol A
per cases ( A <> {} or A = {} ) ;
suppose A <> {} ; :: thesis: 0 <= xvol A
then 0 <= vol A by INTEGRA1:9;
hence 0 <= xvol A by Def2; :: thesis: verum
end;
suppose A = {} ; :: thesis: 0 <= xvol A
hence 0 <= xvol A by Def2; :: thesis: verum
end;
end;