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;