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