theorem Th76: :: BCIALG_1:76

for X being BCI-algebra
for x, y being Element of X st X is alternative holds
( x ` = x & x \ (x \ y) = y & (x \ y) \ y = x )