for E being non empty finite set
for A, B being Event of E st A misses B & A,B are_independent & not prob A = 0 holds
prob B = 0 by Th16, XCMPLX_1:6;