REAL 0 = {(0. (TOP-REAL 0))} by EUCLID:77;