theorem :: FINANCE2:13

REAL \ NAT is Event of Borel_Sets