H1: ( X^2 . 0 = 0. (Z/ 2) & X^2 . 1 = 0. (Z/ 2) ) by qua1;
H2: ( X^2+1 . 0 = 1. (Z/ 2) & X^2+1 . 1 = 0. (Z/ 2) ) by qua1;
H3: ( X^2+X . 0 = 0. (Z/ 2) & X^2+X . 1 = 1. (Z/ 2) ) by qua1;
A1: X^2 <> X^2+1 by H1, qua1;
A2: X^2 <> X^2+X by H1, qua1;
A3: X^2 <> X^2+X+1 by H1, qua1;
A4: X^2+1 <> X^2+X by H2, qua1;
A5: X^2+1 <> X^2+X+1 by H2, qua1;
X^2+X <> X^2+X+1 by H3, qua1;
hence card { p where p is quadratic Polynomial of (Z/ 2) : verum } = 4 by pz2, A1, A2, A3, A4, A5, CARD_2:59; :: thesis: verum