theorem Th7: :: BSPACE:7
(1. Z_2) + (1. Z_2) = 0. Z_2