theorem Th4: :: TOPALG_2:4

for a being Real holds |[a]| /. 1 = a