let X be BCI-algebra; :: thesis: 0. X is positive
(0. X) ` = 0. X by BCIALG_1:2;
then 0. X <= 0. X ;
hence 0. X is positive ; :: thesis: verum