theorem z21: :: FIELD_9:39

( X^2 = X_ *' X_ & Roots X^2 = {(0. (Z/ 2))} )