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 st x <= a \ y holds
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 st x <= a \ y holds
y <= a \ x ) :: thesis: ( ( for a being Element of X st a is being_greatest holds
for x, y being Element of X st x <= a \ y holds
y <= a \ x ) implies X is involutory )

proof

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 st x <= a \ y holds
y <= a \ x
let a be Element of X; :: thesis: ( a is being_greatest implies for x, y being Element of X st x <= a \ y holds
y <= a \ x )
assume A2: a is being_greatest ; :: thesis: for x, y being Element of X st x <= a \ y holds
y <= a \ x
let x, y be Element of X; :: thesis: ( x <= a \ y implies y <= a \ x )
assume x <= a \ y ; :: thesis: y <= a \ x
then x \ (a \ y) = 0. X by BCIALG_1:def 11;
then y \ (a \ x) = 0. X by A1, A2, Th23;
hence y <= a \ x by BCIALG_1:def 11; :: thesis: verum

end;

assume A3: for a being Element of X st a is being_greatest holds
for x, y being Element of X st x <= a \ y holds
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
let x be Element of X; :: thesis: a \ (a \ x) = x
A5: (a \ (a \ x)) \ x = (a \ x) \ (a \ x) by BCIALG_1:7
.= 0. X by BCIALG_1:def 5 ;
(a \ x) \ (a \ x) = 0. X by BCIALG_1:def 5;
then a \ x <= a \ x by BCIALG_1:def 11;
then x <= a \ (a \ x) by A3, A4;
then x \ (a \ (a \ x)) = 0. X by BCIALG_1:def 11;
hence a \ (a \ x) = x by A5, BCIALG_1:def 7; :: thesis: verum