let X be BCI-algebra; :: thesis: ( ex x being Element of X st x is greatest implies for a being Element of X holds a is positive )
given x being Element of X such that A1: x is greatest ; :: thesis: for a being Element of X holds a is positive
0. X <= x by A1, Def5;
then A2: x ` = 0. X by BCIALG_1:def 11;
let a be Element of X; :: thesis: a is positive
a <= x by A1, Def5;
then a \ x = 0. X by BCIALG_1:def 11;
then (a \ x) ` = 0. X by BCIALG_1:def 5;
then (a ` ) \ (0. X) = 0. X by A2, BCIALG_1:9;
then a ` = 0. X by BCIALG_1:2;
then 0. X <= a by BCIALG_1:def 11;
hence a is positive by Def2; :: thesis: verum