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