for a, b being R_eal st a < b holds
ex x being R_eal st
( a < x & x < b & x in REAL )