for Omega being non empty set
for F being SigmaField of Omega
for f, RV being random_variable of F, Borel_Sets
for K being Real holds (f - RV) " [.0,+infty.[ is Element of F