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

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

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

proof

hence
{ [x,y] where x, y is Real : y = - x } is Subset of [:REAL,REAL:]
; :: thesis: verum
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;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