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