theorem Th7: :: BCIALG_5:7

for X being BCI-algebra
for x, y being Element of X holds Polynom (0,0,x,y) = x \ (x \ y)