let x be Element of REAL+ ; :: thesis: ( x <> {} implies [{} ,x] in REAL )
assume A1: x <> {} ; :: thesis: [{} ,x] in REAL

A2: now

assume [{} ,x] in {[{} ,{} ]} ; :: thesis: contradiction
then [{} ,x] = [{} ,{} ] by TARSKI:def 1;
hence contradiction by A1, ZFMISC_1:33; :: thesis: verum

end;

{} in {{} } by TARSKI:def 1;
then [{} ,x] in [:{{} },REAL+ :] by ZFMISC_1:106;
then [{} ,x] in REAL+ \/ [:{{} },REAL+ :] by XBOOLE_0:def 3;
hence [{} ,x] in REAL by A2, NUMBERS:def 1, XBOOLE_0:def 5; :: thesis: verum