let X be BCI-algebra; :: thesis: 0. X is minimal
for x being Element of X st x \ (0. X) = 0. X holds
x = 0. X by BCIALG_1:2;
hence 0. X is minimal by BCIALG_1:def 14; :: thesis: verum