theorem :: RPR_1:17

for E being non empty finite set
for A being Event of E holds prob A <= 1