theorem Th28: :: BCIALG_2:28

for X being BCI-algebra
for x being Element of X holds x \ ((x `) `) is positive Element of X