theorem :: RPR_1:15

for E being non empty finite set holds prob ([#] E) = 1 by XCMPLX_1:60;