let X be BCI-algebra; :: thesis: ( ( for x, y being Element of X holds (x \ y) \ (y \ x) in BCK-part X ) implies X is quasi-associative )

assume A1: for x, y being Element of X holds (x \ y) \ (y \ x) in BCK-part X ; :: thesis: X is quasi-associative

for x being Element of X holds (x `) ` = x `

assume A1: for x, y being Element of X holds (x \ y) \ (y \ x) in BCK-part X ; :: thesis: X is quasi-associative

for x being Element of X holds (x `) ` = x `

proof

hence
X is quasi-associative
; :: thesis: verum
let x be Element of X; :: thesis: (x `) ` = x `

x \ (x `) = (x \ (0. X)) \ (x `) by Th2;

then x \ (x `) in { x2 where x2 is Element of X : 0. X <= x2 } by A1;

then ex x2 being Element of X st

( x \ (x `) = x2 & 0. X <= x2 ) ;

then (x \ (x `)) ` = 0. X ;

then A2: (x `) \ ((x `) `) = 0. X by Th9;

(x `) \ x = (x `) \ (x \ (0. X)) by Th2;

then (x `) \ x in { x1 where x1 is Element of X : 0. X <= x1 } by A1;

then ex x1 being Element of X st

( (x `) \ x = x1 & 0. X <= x1 ) ;

then ((x `) \ x) ` = 0. X ;

then ((x `) `) \ (x `) = 0. X by Th9;

hence (x `) ` = x ` by A2, Def7; :: thesis: verum

end;x \ (x `) = (x \ (0. X)) \ (x `) by Th2;

then x \ (x `) in { x2 where x2 is Element of X : 0. X <= x2 } by A1;

then ex x2 being Element of X st

( x \ (x `) = x2 & 0. X <= x2 ) ;

then (x \ (x `)) ` = 0. X ;

then A2: (x `) \ ((x `) `) = 0. X by Th9;

(x `) \ x = (x `) \ (x \ (0. X)) by Th2;

then (x `) \ x in { x1 where x1 is Element of X : 0. X <= x1 } by A1;

then ex x1 being Element of X st

( (x `) \ x = x1 & 0. X <= x1 ) ;

then ((x `) \ x) ` = 0. X ;

then ((x `) `) \ (x `) = 0. X by Th9;

hence (x `) ` = x ` by A2, Def7; :: thesis: verum