theorem Th12: :: BCIALG_4:13

for X being BCI-Algebra_with_Condition(S)
for x, y being Element of X holds y <= x * (y \ x)