let x, y be Real; :: thesis: ( [x,y] in real-anti-diagonal implies y = - x )
assume [x,y] in real-anti-diagonal ; :: thesis: y = - x
then consider x1, y1 being Real such that
A1: [x,y] = [x1,y1] and
A2: y1 = - x1 ;
( x = x1 & y = y1 ) by A1, XTUPLE_0:1;
hence y = - x by A2; :: thesis: verum