reconsider a = 1 as Element of REAL by NUMBERS:19;
consider myp1 being Element of REAL such that
A2: myp1 = - a ;
thus ( 1 in REAL & - 1 in REAL ) by A2; :: thesis: verum