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