let Omega be non empty set ; :: thesis: 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
let F be SigmaField of Omega; :: thesis: for f, RV being random_variable of F, Borel_Sets
for K being Real holds (f - RV) " [.0,+infty.[ is Element of F
let f, RV be random_variable of F, Borel_Sets ; :: thesis: for K being Real holds (f - RV) " [.0,+infty.[ is Element of F
let K be Real; :: thesis: (f - RV) " [.0,+infty.[ is Element of F
A1: [.0,+infty.[ is Element of Borel_Sets by FINANCE1:3;
f - RV is random_variable of F, Borel_Sets by FINANCE2:24;
then f - RV is_random_variable_on F, Borel_Sets by RANDOM_3:def 1;
hence (f - RV) " [.0,+infty.[ is Element of F by A1; :: thesis: verum