assume REAL+ meets [:{{} },REAL+ :] ; :: thesis: contradiction
then consider x being set such that
A1: x in REAL+ and
A2: x in [:{{} },REAL+ :] by XBOOLE_0:3;
consider x1, x2 being set such that
A3: x1 in {{} } and
x2 in REAL+ and
A4: x = [x1,x2] by A2, ZFMISC_1:103;
x1 = {} by A3, TARSKI:def 1;
hence contradiction by A1, A4, ARYTM_2:3; :: thesis: verum