Is there a formalization of probability theory so that the product definition of independence is a conclusion, not the definition? – mathoverflow.net

If real random variables X, Y (with cdf's FX and FY) are each defined on a probability space (𝛀,ℬ,P), they are defined to be independent precisely when their joint cumulative distribution F(s,t) = ...