theorem Th17: :: PROB_2:17

for Omega being non empty set
for Sigma being SigmaField of Omega
for A being Event of Sigma
for P being Probability of Sigma holds
( P . A < 1 iff 0 < P . (([#] Sigma) \ A) )