theorem :: BCIALG_2:29

for X being BCI-algebra
for a being Element of X holds
( a is minimal iff (a `) ` = a )