let X be BCI-algebra; :: thesis: ( 0. X is maximal implies for a being Element of X holds a is minimal )
assume A1: 0. X is maximal ; :: thesis: for a being Element of X holds a is minimal
let a be Element of X; :: thesis: a is minimal

now

let x be Element of X; :: thesis: ( x <= a implies x = a )
assume x <= a ; :: thesis: x = a
then A2: x \ a = 0. X by BCIALG_1:def 11;
then (a \ x) ` = 0. X by BCIALG_1:6;
then 0. X <= a \ x by BCIALG_1:def 11;
then 0. X = a \ x by A1, Def4;
hence x = a by A2, BCIALG_1:def 7; :: thesis: verum

end;

hence a is minimal by Lm1; :: thesis: verum