theorem Th5: :: FIELD_3:4
(1. (Z/ 2)) + (1. (Z/ 2)) = 0. (Z/ 2)