theorem Th45: :: RPR_1:45
for E being non empty finite set
for A, B being Event of E st 0 < prob B & A misses B holds
prob ((A `),B) = 1