let X be BCK-Algebra_with_Condition(S); :: thesis: ( X is implicative iff ( X is commutative & X is positive-implicative ) )

thus ( X is implicative implies ( X is commutative & X is positive-implicative ) ) :: thesis: ( X is commutative & X is positive-implicative implies X is implicative )

A5: X is commutative and

A6: X is positive-implicative ; :: thesis: X is implicative

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

thus ( X is implicative implies ( X is commutative & X is positive-implicative ) ) :: thesis: ( X is commutative & X is positive-implicative implies X is implicative )

proof

assume that
assume A1:
X is implicative
; :: thesis: ( X is commutative & X is positive-implicative )

A2: for x, y being Element of X holds x \ (x \ y) <= y \ (y \ x)

end;A2: for x, y being Element of X holds x \ (x \ y) <= y \ (y \ x)

proof

A3:
for x, y being Element of X holds x \ (x \ y) = y \ (y \ x)
let x, y be Element of X; :: thesis: x \ (x \ y) <= y \ (y \ x)

(x \ (x \ y)) \ y = (x \ y) \ (x \ y) by BCIALG_1:7

.= 0. X by BCIALG_1:def 5 ;

then x \ (x \ y) <= y ;

then (x \ (x \ y)) \ (y \ x) <= y \ (y \ x) by BCIALG_1:5;

then (x \ (y \ x)) \ (x \ y) <= y \ (y \ x) by BCIALG_1:7;

hence x \ (x \ y) <= y \ (y \ x) by A1; :: thesis: verum

end;(x \ (x \ y)) \ y = (x \ y) \ (x \ y) by BCIALG_1:7

.= 0. X by BCIALG_1:def 5 ;

then x \ (x \ y) <= y ;

then (x \ (x \ y)) \ (y \ x) <= y \ (y \ x) by BCIALG_1:5;

then (x \ (y \ x)) \ (x \ y) <= y \ (y \ x) by BCIALG_1:7;

hence x \ (x \ y) <= y \ (y \ x) by A1; :: thesis: verum

proof

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

y \ (y \ x) <= x \ (x \ y) by A2;

then A4: (y \ (y \ x)) \ (x \ (x \ y)) = 0. X ;

x \ (x \ y) <= y \ (y \ x) by A2;

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

hence x \ (x \ y) = y \ (y \ x) by A4, BCIALG_1:def 7; :: thesis: verum

end;y \ (y \ x) <= x \ (x \ y) by A2;

then A4: (y \ (y \ x)) \ (x \ (x \ y)) = 0. X ;

x \ (x \ y) <= y \ (y \ x) by A2;

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

hence x \ (x \ y) = y \ (y \ x) by A4, BCIALG_1:def 7; :: thesis: verum

proof

hence
( X is commutative & X is positive-implicative )
by A3; :: thesis: verum
let x, y be Element of X; :: thesis: x \ y = (x \ y) \ y

(x \ y) \ (y \ (x \ y)) = x \ y by A1;

hence x \ y = (x \ y) \ y by A1; :: thesis: verum

end;(x \ y) \ (y \ (x \ y)) = x \ y by A1;

hence x \ y = (x \ y) \ y by A1; :: thesis: verum

A5: X is commutative and

A6: X is positive-implicative ; :: thesis: X is implicative

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

proof

hence
X is implicative
; :: thesis: verum
let x, y be Element of X; :: thesis: x \ (y \ x) = x

x \ (x \ (x \ (y \ x))) = x \ (y \ x) by BCIALG_1:8;

then A7: x \ (y \ x) = x \ ((y \ x) \ ((y \ x) \ x)) by A5;

(y \ x) \ ((y \ x) \ x) = (y \ x) \ (y \ x) by A6

.= 0. X by BCIALG_1:def 5 ;

hence x \ (y \ x) = x by A7, BCIALG_1:2; :: thesis: verum

end;x \ (x \ (x \ (y \ x))) = x \ (y \ x) by BCIALG_1:8;

then A7: x \ (y \ x) = x \ ((y \ x) \ ((y \ x) \ x)) by A5;

(y \ x) \ ((y \ x) \ x) = (y \ x) \ (y \ x) by A6

.= 0. X by BCIALG_1:def 5 ;

hence x \ (y \ x) = x by A7, BCIALG_1:2; :: thesis: verum