let y be set ; :: thesis: ( [{} ,y] in REAL implies y <> {} )
assume that
A1: [{} ,y] in REAL and
A2: y = {} ; :: thesis: contradiction
[{} ,y] in {[{} ,{} ]} by A2, TARSKI:def 1;
hence contradiction by A1, NUMBERS:def 1, XBOOLE_0:def 5; :: thesis: verum