for Omega being non empty set
for Sigma being SigmaField of Omega
for X, Y being random_variable of Sigma, Borel_Sets holds X - Y is random_variable of Sigma, Borel_Sets