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
let a be Element of X; :: thesis: a is positive
a <= x by A1;
then a \ x = 0. X ;
then A2: (a \ x) ` = 0. X by BCIALG_1:def 5;
0. X <= x by A1;
then x ` = 0. X ;
then (a `) \ (0. X) = 0. X by A2, BCIALG_1:9;
then a ` = 0. X by BCIALG_1:2;
then 0. X <= a ;
hence a is positive ; :: thesis: verum