theorem Th29: :: PROB_2:29

for Omega being non empty set
for Sigma being SigmaField of Omega
for P being Probability of Sigma
for B, A being Event of Sigma st 0 < P . B holds
P . (A /\ B) = ((P .|. B) . A) * (P . B)