let X be commutative BCK-Algebra_with_Condition(S); :: thesis: for a being Element of X st a is greatest holds
for x, y being Element of X holds x * y = a \ ((a \ x) \ y)
let a be Element of X; :: thesis: ( a is greatest implies for x, y being Element of X holds x * y = a \ ((a \ x) \ y) )
assume A1: a is greatest ; :: thesis: for x, y being Element of X holds x * y = a \ ((a \ x) \ y)
for x, y being Element of X holds x * y = a \ ((a \ x) \ y)

proof

let x, y be Element of X; :: thesis: x * y = a \ ((a \ x) \ y)
A2: x * y <= a by A1, BCIALG_2:def 5;
a \ ((a \ x) \ y) = a \ (a \ (x * y)) by Th11
.= (x * y) \ ((x * y) \ a) by Def9
.= (x * y) \ (0. X) by A2 ;
hence x * y = a \ ((a \ x) \ y) by BCIALG_1:2; :: thesis: verum

end;

hence for x, y being Element of X holds x * y = a \ ((a \ x) \ y) ; :: thesis: verum