theorem Th44: :: BCIALG_4:45

for X being BCK-Algebra_with_Condition(S) holds
( X is positive-implicative iff for x being Element of X holds x * x = x )