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)

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

hence
for x, y being Element of X holds x * y = a \ ((a \ x) \ y)
; :: thesis: verum
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;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