theorem cz2: :: FIELD_9:34

the carrier of (Z/ 2) = {(0. (Z/ 2)),(1. (Z/ 2))}