set M = {<%(0. (Z/ 2)),(0. (Z/ 2)),(1. (Z/ 2))%>,<%(1. (Z/ 2)),(0. (Z/ 2)),(1. (Z/ 2))%>,<%(0. (Z/ 2)),(1. (Z/ 2)),(1. (Z/ 2))%>,<%(1. (Z/ 2)),(1. (Z/ 2)),(1. (Z/ 2))%>};

A: now :: thesis: for o being object st o in {<%(0. (Z/ 2)),(0. (Z/ 2)),(1. (Z/ 2))%>,<%(1. (Z/ 2)),(0. (Z/ 2)),(1. (Z/ 2))%>,<%(0. (Z/ 2)),(1. (Z/ 2)),(1. (Z/ 2))%>,<%(1. (Z/ 2)),(1. (Z/ 2)),(1. (Z/ 2))%>} holds
o in { p where p is quadratic Polynomial of (Z/ 2) : verum }

let o be object ; :: thesis: ( o in {<%(0. (Z/ 2)),(0. (Z/ 2)),(1. (Z/ 2))%>,<%(1. (Z/ 2)),(0. (Z/ 2)),(1. (Z/ 2))%>,<%(0. (Z/ 2)),(1. (Z/ 2)),(1. (Z/ 2))%>,<%(1. (Z/ 2)),(1. (Z/ 2)),(1. (Z/ 2))%>} implies o in { p where p is quadratic Polynomial of (Z/ 2) : verum } )
assume o in {<%(0. (Z/ 2)),(0. (Z/ 2)),(1. (Z/ 2))%>,<%(1. (Z/ 2)),(0. (Z/ 2)),(1. (Z/ 2))%>,<%(0. (Z/ 2)),(1. (Z/ 2)),(1. (Z/ 2))%>,<%(1. (Z/ 2)),(1. (Z/ 2)),(1. (Z/ 2))%>} ; :: thesis: o in { p where p is quadratic Polynomial of (Z/ 2) : verum }
then o is quadratic Polynomial of (Z/ 2) by ENUMSET1:def 2;
hence o in { p where p is quadratic Polynomial of (Z/ 2) : verum } ; :: thesis: verum

end;

now :: thesis: for o being object st o in { q where q is quadratic Polynomial of (Z/ 2) : verum } holds
o in {<%(0. (Z/ 2)),(0. (Z/ 2)),(1. (Z/ 2))%>,<%(1. (Z/ 2)),(0. (Z/ 2)),(1. (Z/ 2))%>,<%(0. (Z/ 2)),(1. (Z/ 2)),(1. (Z/ 2))%>,<%(1. (Z/ 2)),(1. (Z/ 2)),(1. (Z/ 2))%>}

let o be object ; :: thesis: ( o in { q where q is quadratic Polynomial of (Z/ 2) : verum } implies b₁ in {<%(0. (Z/ 2)),(0. (Z/ 2)),(1. (Z/ 2))%>,<%(1. (Z/ 2)),(0. (Z/ 2)),(1. (Z/ 2))%>,<%(0. (Z/ 2)),(1. (Z/ 2)),(1. (Z/ 2))%>,<%(1. (Z/ 2)),(1. (Z/ 2)),(1. (Z/ 2))%>} )
assume o in { q where q is quadratic Polynomial of (Z/ 2) : verum } ; :: thesis: b₁ in {<%(0. (Z/ 2)),(0. (Z/ 2)),(1. (Z/ 2))%>,<%(1. (Z/ 2)),(0. (Z/ 2)),(1. (Z/ 2))%>,<%(0. (Z/ 2)),(1. (Z/ 2)),(1. (Z/ 2))%>,<%(1. (Z/ 2)),(1. (Z/ 2)),(1. (Z/ 2))%>}
then consider p being quadratic Polynomial of (Z/ 2) such that
A1: o = p ;
consider b, c being Element of (Z/ 2) such that
A2: p = <%c,b,(1. (Z/ 2))%> by qua5a;

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

suppose A3: b = 1. (Z/ 2) ; :: thesis: b₁ in {<%(0. (Z/ 2)),(0. (Z/ 2)),(1. (Z/ 2))%>,<%(1. (Z/ 2)),(0. (Z/ 2)),(1. (Z/ 2))%>,<%(0. (Z/ 2)),(1. (Z/ 2)),(1. (Z/ 2))%>,<%(1. (Z/ 2)),(1. (Z/ 2)),(1. (Z/ 2))%>}

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

suppose c = 1. (Z/ 2) ; :: thesis: b₁ in {<%(0. (Z/ 2)),(0. (Z/ 2)),(1. (Z/ 2))%>,<%(1. (Z/ 2)),(0. (Z/ 2)),(1. (Z/ 2))%>,<%(0. (Z/ 2)),(1. (Z/ 2)),(1. (Z/ 2))%>,<%(1. (Z/ 2)),(1. (Z/ 2)),(1. (Z/ 2))%>}

hence o in {<%(0. (Z/ 2)),(0. (Z/ 2)),(1. (Z/ 2))%>,<%(1. (Z/ 2)),(0. (Z/ 2)),(1. (Z/ 2))%>,<%(0. (Z/ 2)),(1. (Z/ 2)),(1. (Z/ 2))%>,<%(1. (Z/ 2)),(1. (Z/ 2)),(1. (Z/ 2))%>} by A3, A2, A1, ENUMSET1:def 2; :: thesis: verum

end;

suppose c = 0. (Z/ 2) ; :: thesis: b₁ in {<%(0. (Z/ 2)),(0. (Z/ 2)),(1. (Z/ 2))%>,<%(1. (Z/ 2)),(0. (Z/ 2)),(1. (Z/ 2))%>,<%(0. (Z/ 2)),(1. (Z/ 2)),(1. (Z/ 2))%>,<%(1. (Z/ 2)),(1. (Z/ 2)),(1. (Z/ 2))%>}

hence o in {<%(0. (Z/ 2)),(0. (Z/ 2)),(1. (Z/ 2))%>,<%(1. (Z/ 2)),(0. (Z/ 2)),(1. (Z/ 2))%>,<%(0. (Z/ 2)),(1. (Z/ 2)),(1. (Z/ 2))%>,<%(1. (Z/ 2)),(1. (Z/ 2)),(1. (Z/ 2))%>} by A3, A2, A1, ENUMSET1:def 2; :: thesis: verum

end;

end;

end;

suppose A3: b = 0. (Z/ 2) ; :: thesis: b₁ in {<%(0. (Z/ 2)),(0. (Z/ 2)),(1. (Z/ 2))%>,<%(1. (Z/ 2)),(0. (Z/ 2)),(1. (Z/ 2))%>,<%(0. (Z/ 2)),(1. (Z/ 2)),(1. (Z/ 2))%>,<%(1. (Z/ 2)),(1. (Z/ 2)),(1. (Z/ 2))%>}

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

suppose c = 1. (Z/ 2) ; :: thesis: b₁ in {<%(0. (Z/ 2)),(0. (Z/ 2)),(1. (Z/ 2))%>,<%(1. (Z/ 2)),(0. (Z/ 2)),(1. (Z/ 2))%>,<%(0. (Z/ 2)),(1. (Z/ 2)),(1. (Z/ 2))%>,<%(1. (Z/ 2)),(1. (Z/ 2)),(1. (Z/ 2))%>}

hence o in {<%(0. (Z/ 2)),(0. (Z/ 2)),(1. (Z/ 2))%>,<%(1. (Z/ 2)),(0. (Z/ 2)),(1. (Z/ 2))%>,<%(0. (Z/ 2)),(1. (Z/ 2)),(1. (Z/ 2))%>,<%(1. (Z/ 2)),(1. (Z/ 2)),(1. (Z/ 2))%>} by A3, A2, A1, ENUMSET1:def 2; :: thesis: verum

end;

suppose c = 0. (Z/ 2) ; :: thesis: b₁ in {<%(0. (Z/ 2)),(0. (Z/ 2)),(1. (Z/ 2))%>,<%(1. (Z/ 2)),(0. (Z/ 2)),(1. (Z/ 2))%>,<%(0. (Z/ 2)),(1. (Z/ 2)),(1. (Z/ 2))%>,<%(1. (Z/ 2)),(1. (Z/ 2)),(1. (Z/ 2))%>}

hence o in {<%(0. (Z/ 2)),(0. (Z/ 2)),(1. (Z/ 2))%>,<%(1. (Z/ 2)),(0. (Z/ 2)),(1. (Z/ 2))%>,<%(0. (Z/ 2)),(1. (Z/ 2)),(1. (Z/ 2))%>,<%(1. (Z/ 2)),(1. (Z/ 2)),(1. (Z/ 2))%>} by A3, A2, A1, ENUMSET1:def 2; :: thesis: verum

end;

end;

end;

end;

end;

hence { p where p is quadratic Polynomial of (Z/ 2) : verum } = {X^2,X^2+1,X^2+X,X^2+X+1} by A, TARSKI:2; :: thesis: verum