:: deftheorem defines MULT211 GATE_5:def 2 :
for x0, x1, y0, y1 being set holds MULT211 (x1,y1,x0,y0) = ADD1 ((AND2 (x1,y0)),(AND2 (x0,y1)),{});