let E be non empty finite set ; :: thesis: for A being Event of E holds prob (A ` ),A = 0
let A be Event of E; :: thesis: prob (A ` ),A = 0
A ` misses A by SUBSET_1:44;
then prob ((A ` ) /\ A) = 0 by Th41;
hence prob (A ` ),A = 0 ; :: thesis: verum