theorem :: JORDAN2C:105

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