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