Yes, that's right. And it seems that essentially the same argument proves additivity of area-under-graph integral (first, you take "undergraphs" of simple functions, then you take their union).

On the other hand, additivity of integral isn't obvious under the standard definition as well, since you first have to prove that a sum of two measurable functions is measurable and I think that the additivity for areas under the graph could involve a similar argument.

@Qfwfq You're right. This is essentially the answer of Nik Weaver. I missed it, because I expected some counterexample.

How do you find it in practice (if you know the book)? Does the author struggle with some added difficulties?

@ArturoMagidin Ok, then you want to apply it to some examples, where Riemann integration (or Riemann integration modulo a set of measure 0) doesn't apply. I would be happy to see some examples, where Lebesgue integral is easier to compute than the measure of the are under graph. This is a part of what I'm asking.

Right, right, right. Ok, sorry for my mistake.

There are uncountably many of $X_a$, so I'm not sure i follow your argument.

@ArturoMagidin You show that your new integral is the same as Riemann integral whenever applicable, the same way you do it for Lebesgue integral.

@ArturoMagidin Well, once you defined Lebesgue measure, you can define area under graph as measure of the set of points under graph. EDIT: I've written a couple of seconds too late.

Well, for example maps may well given by power series which you can compute by some complicated recursion. It would be very surprising if this fact really required choice.

I think one natural reformulation of the question is a s follows: Look at the set of all formulae $\phi$ such that provably in ZFC they define a cardinal and ZFC proves $\forall x \ \ \phi(x) \rightarrow x > 2^{\aleph_0}$. On these formulae you have a partial order: $\phi \leq \psi$ if provably in ZFC the inequality holds between the elements defined with the formulae. Note that this is not a linear order and it isn't well-founded. Does this set have a minimum? Can you characterise it? As I see it, it has nothing to do with Solovay's theorem.

@YCor "Such that it is provable in ZFC" obviously is a formula of ZFC. Although I do agree that the question could be clarified a bit.

In this case it's probably a slight overkill, but the answer to your first question is yes for general reasons. If every egal run of a game is finite, then exactly one of the players (the one that starts or the second one) has a winning strategy.