set p = <%(1. (Z/ 2)),(1. (Z/ 2)),(1. (Z/ 2))%>;
set a = the Element of Roots <%(1. (Z/ 2)),(1. (Z/ 2)),(1. (Z/ 2))%>;

now :: thesis: not Roots <%(1. (Z/ 2)),(1. (Z/ 2)),(1. (Z/ 2))%> <> {}

assume A: Roots <%(1. (Z/ 2)),(1. (Z/ 2)),(1. (Z/ 2))%> <> {} ; :: thesis: contradiction
then the Element of Roots <%(1. (Z/ 2)),(1. (Z/ 2)),(1. (Z/ 2))%> in Roots <%(1. (Z/ 2)),(1. (Z/ 2)),(1. (Z/ 2))%> ;
then reconsider a = the Element of Roots <%(1. (Z/ 2)),(1. (Z/ 2)),(1. (Z/ 2))%> as Element of (Z/ 2) ;
B: a is_a_root_of <%(1. (Z/ 2)),(1. (Z/ 2)),(1. (Z/ 2))%> by A, POLYNOM5:def 10;

per cases ( a = 0. (Z/ 2) or a = 1. (Z/ 2) ) by cz2, TARSKI:def 2;

suppose a = 0. (Z/ 2) ; :: thesis: contradiction

then eval (<%(1. (Z/ 2)),(1. (Z/ 2)),(1. (Z/ 2))%>,a) = ((1. (Z/ 2)) + ((1. (Z/ 2)) * (0. (Z/ 2)))) + ((1. (Z/ 2)) * ((0. (Z/ 2)) ^2)) by evalq
.= 1. (Z/ 2) ;
hence contradiction by B; :: thesis: verum

end;

suppose a = 1. (Z/ 2) ; :: thesis: contradiction

then eval (<%(1. (Z/ 2)),(1. (Z/ 2)),(1. (Z/ 2))%>,a) = ((1. (Z/ 2)) + ((1. (Z/ 2)) * (1. (Z/ 2)))) + ((1. (Z/ 2)) * ((1. (Z/ 2)) ^2)) by evalq
.= (1. (Z/ 2)) + (0. (Z/ 2)) by FIELD_3:4 ;
hence contradiction by B; :: thesis: verum

end;

end;

end;

hence Roots X^2+X+1 = {} ; :: thesis: verum