theorem Th16: :: RPR_1:16

for E being non empty finite set
for A, B being Event of E st A misses B holds
prob (A /\ B) = 0 by CARD_1:27;