theorem Th37: :: BCIALG_4:38

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