REAL = ].-infty,+infty.[ by XXREAL_1:224;
hence REAL is open_interval Subset of REAL by MEASURE5:def 2; :: thesis: verum