theorem Th53: :: TOPREALC:53

TIMES 0 = [:(TOP-REAL 0),(TOP-REAL 0):] --> (0. (TOP-REAL 0))