let E be non empty finite set ; :: thesis: prob ([#] E) = 1
card E <> 0 by Lm1;
hence prob ([#] E) = 1 by XCMPLX_1:60; :: thesis: verum