:: deftheorem Def6 defines .|. PROB_2:def 6 :
for Omega being non empty set
for Sigma being SigmaField of Omega
for P being Probability of Sigma
for B being Event of Sigma st 0 < P . B holds
for b₅ being Probability of Sigma holds
( b₅ = P .|. B iff for A being Event of Sigma holds b₅ . A = (P . (A /\ B)) / (P . B) );