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, XBOOLE_0:def 5; :: thesis: verum