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

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

end;

assume A2: (a ` ) ` = a ; :: thesis: a is minimal

now

let x be Element of X; :: thesis: ( x <= a implies x = a )
assume x <= a ; :: thesis: x = a
then A3: x \ a = 0. X by BCIALG_1:def 11;
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