let X be bounded BCK-algebra; :: thesis: ( X is involutory iff for a being Element of X st a is being_greatest holds

for x, y being Element of X holds x \ y = (a \ y) \ (a \ x) )

thus ( X is involutory implies for a being Element of X st a is being_greatest holds

for x, y being Element of X holds x \ y = (a \ y) \ (a \ x) ) :: thesis: ( ( for a being Element of X st a is being_greatest holds

for x, y being Element of X holds x \ y = (a \ y) \ (a \ x) ) implies X is involutory )

for x, y being Element of X holds x \ y = (a \ y) \ (a \ x) ; :: thesis: X is involutory

let a be Element of X; :: according to BCIALG_3:def 7 :: thesis: ( a is being_greatest implies for x being Element of X holds a \ (a \ x) = x )

assume A4: a is being_greatest ; :: thesis: for x being Element of X holds a \ (a \ x) = x

for x, y being Element of X holds x \ y = (a \ y) \ (a \ x) )

thus ( X is involutory implies for a being Element of X st a is being_greatest holds

for x, y being Element of X holds x \ y = (a \ y) \ (a \ x) ) :: thesis: ( ( for a being Element of X st a is being_greatest holds

for x, y being Element of X holds x \ y = (a \ y) \ (a \ x) ) implies X is involutory )

proof

assume A3:
for a being Element of X st a is being_greatest holds
assume A1:
X is involutory
; :: thesis: for a being Element of X st a is being_greatest holds

for x, y being Element of X holds x \ y = (a \ y) \ (a \ x)

let a be Element of X; :: thesis: ( a is being_greatest implies for x, y being Element of X holds x \ y = (a \ y) \ (a \ x) )

assume A2: a is being_greatest ; :: thesis: for x, y being Element of X holds x \ y = (a \ y) \ (a \ x)

for x, y being Element of X holds x \ y = (a \ y) \ (a \ x)

end;for x, y being Element of X holds x \ y = (a \ y) \ (a \ x)

let a be Element of X; :: thesis: ( a is being_greatest implies for x, y being Element of X holds x \ y = (a \ y) \ (a \ x) )

assume A2: a is being_greatest ; :: thesis: for x, y being Element of X holds x \ y = (a \ y) \ (a \ x)

for x, y being Element of X holds x \ y = (a \ y) \ (a \ x)

proof

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

x \ y = (a \ (a \ x)) \ y by A1, A2

.= (a \ y) \ (a \ x) by BCIALG_1:7 ;

hence x \ y = (a \ y) \ (a \ x) ; :: thesis: verum

end;x \ y = (a \ (a \ x)) \ y by A1, A2

.= (a \ y) \ (a \ x) by BCIALG_1:7 ;

hence x \ y = (a \ y) \ (a \ x) ; :: thesis: verum

for x, y being Element of X holds x \ y = (a \ y) \ (a \ x) ; :: thesis: X is involutory

let a be Element of X; :: according to BCIALG_3:def 7 :: thesis: ( a is being_greatest implies for x being Element of X holds a \ (a \ x) = x )

assume A4: a is being_greatest ; :: thesis: for x being Element of X holds a \ (a \ x) = x

now :: thesis: for x being Element of X holds a \ (a \ x) = x

hence
for x being Element of X holds a \ (a \ x) = x
; :: thesis: verumlet x be Element of X; :: thesis: a \ (a \ x) = x

(a \ (a \ x)) \ (0. X) = (a \ (0. X)) \ (a \ x) by BCIALG_1:7

.= x \ (0. X) by A3, A4

.= x by BCIALG_1:2 ;

hence a \ (a \ x) = x by BCIALG_1:2; :: thesis: verum

end;(a \ (a \ x)) \ (0. X) = (a \ (0. X)) \ (a \ x) by BCIALG_1:7

.= x \ (0. X) by A3, A4

.= x by BCIALG_1:2 ;

hence a \ (a \ x) = x by BCIALG_1:2; :: thesis: verum