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

A2: now :: thesis: not [{},x] in {[{},{}]}

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

end;

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