let E be non empty finite set ; :: thesis: prob (([#] E),([#] E)) = 1
prob ([#] E) = 1 by XCMPLX_1:60;
hence prob (([#] E),([#] E)) = 1 ; :: thesis: verum