let X be BCI-algebra; :: thesis: for a being Element of X holds
( a is minimal iff ex x being Element of X st a = x ` )
let a be Element of X; :: thesis: ( a is minimal iff ex x being Element of X st a = x ` )
thus ( a is minimal implies ex x being Element of X st a = x ` ) :: thesis: ( ex x being Element of X st a = x ` implies a is minimal )

proof

assume A1: a is minimal ; :: thesis: ex x being Element of X st a = x `
take x = a ` ; :: thesis: a = x `
(x `) \ a = 0. X by BCIALG_1:1;
then x ` <= a ;
hence a = x ` by A1; :: thesis: verum

end;

given x being Element of X such that A2: a = x ` ; :: thesis: a is minimal

now :: thesis: for y being Element of X st y <= a holds
a = y

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

end;

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