:: deftheorem defines MULT310 GATE_5:def 5 :
for x0, x1, x2, y0, y1 being set holds MULT310 (x2,x1,y1,x0,y0) = AND2 (x0,y0);