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

proof

((a `) `) \ a = 0. X by BCIALG_1:1;
then A1: (a `) ` <= a ;
assume a is minimal ; :: thesis: (a `) ` = a
hence (a `) ` = a by A1; :: thesis: verum

end;

assume A2: (a `) ` = a ; :: 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 A3: x \ a = 0. X ;
a \ x = (x `) \ (a `) by A2, BCIALG_1:7;
then a \ x = (0. X) ` by A3, BCIALG_1:9;
then a \ x = 0. X by BCIALG_1:def 5;
hence x = a by A3, BCIALG_1:def 7; :: thesis: verum

end;

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