theorem :: BCIALG_2:33

for X being BCI-algebra
for x being Element of X
for n being Nat holds ((0. X),(x `)) to_power n is minimal