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