reconsider e = 2 as prime Nat by INT_2:28;
set F = Z/ e;
take Z/ e ; :: thesis: Z/ e is 2 -characteristic
thus Z/ e is 2 -characteristic ; :: thesis: verum