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

proof

assume A1: a is minimal ; :: 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 x \ a = 0. X by BCIALG_1:def 11;
hence x = a by A1, BCIALG_1:def 14; :: thesis: verum

end;

assume A2: for x being Element of X st x <= a holds
x = a ; :: thesis: a is minimal

now

let y be Element of X; :: thesis: ( y \ a = 0. X implies y = a )
assume y \ a = 0. X ; :: thesis: y = a
then y <= a by BCIALG_1:def 11;
hence y = a by A2; :: thesis: verum

end;

hence a is minimal by BCIALG_1:def 14; :: thesis: verum