theorem :: BCIALG_2:23

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