for a, b, c, d being Real holds not (0,1,2,3) --> (a,b,c,d) in COMPLEX