for z being R_eal holds
( z in REAL iff - z in REAL )