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 :: thesis: for x being Element of X st x <= a holds
x = a

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

end;

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