for Omega being non empty set
for F being SigmaField of Omega
for RV being random_variable of F, Borel_Sets
for K being Real
for w being Element of Omega holds (Straddle (RV,K)) . w = |.((RV - (Omega --> K)) . w).|