theorem :: RPR_1:42

for E being non empty finite set
for B being Event of E st 0 < prob B holds
prob (([#] E),B) = 1 by Th41;