set L = { [x,y] where x, y is Real : y = - x } ;
{ [x,y] where x, y is Real : y = - x } c= [:REAL,REAL:]

proof

let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in { [x,y] where x, y is Real : y = - x } or z in [:REAL,REAL:] )
assume z in { [x,y] where x, y is Real : y = - x } ; :: thesis: z in [:REAL,REAL:]
then consider x, y being Real such that
A1: z = [x,y] and
y = - x ;
( x in REAL & y in REAL ) by XREAL_0:def 1;
hence z in [:REAL,REAL:] by A1, ZFMISC_1:87; :: thesis: verum

end;

hence { [x,y] where x, y is Real : y = - x } is Subset of [:REAL,REAL:] ; :: thesis: verum