theorem :: BCIALG_4:3

for X being non empty BCIStr_1 holds
( ( X is BCI-algebra & ( for x, y being Element of X holds
( (x * y) \ x <= y & ( for t being Element of X st t \ x <= y holds
t <= x * y ) ) ) ) iff X is BCI-Algebra_with_Condition(S) ) by Lm2, Lm3;