:: deftheorem defines prob RPR_1:def 2 :
for E being finite set
for B, A being Event of E holds prob (A,B) = (prob (A /\ B)) / (prob B);