0 in {0} by TARSKI:def 1;
hence for x being Element of REAL+ holds [0,x] in [:{0},REAL+:] by ZFMISC_1:87; :: thesis: verum