X --> the Probability of S is S -Probability_valued Function by Lm1;
hence ex b₁ being X -defined S -Probability_valued Function st b₁ is total ; :: thesis: verum