theorem Th5: :: TOPREALB:5
R^1 | (R^1 ([#] REAL)) = R^1