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