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:24;
then prob (A /\ (A `)) = 0 by Th16;
hence prob (A,(A `)) = 0 ; :: thesis: verum