for x, y being Element of REAL st [*x,y*] in REAL holds
y = 0