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