theorem :: RPR_1:37

for E being non empty finite set
for A, B being Event of E st 0 < prob B & A c= B holds
prob (A,B) = (prob A) / (prob B)