theorem :: EUCLID:77

REAL 0 = {(0. (TOP-REAL 0))}