let X be BCK-algebra; :: thesis: for I being Ideal of X st I is implicative-ideal of X holds

( I is commutative Ideal of X & I is positive-implicative-ideal of X )

let I be Ideal of X; :: thesis: ( I is implicative-ideal of X implies ( I is commutative Ideal of X & I is positive-implicative-ideal of X ) )

assume A1: I is implicative-ideal of X ; :: thesis: ( I is commutative Ideal of X & I is positive-implicative-ideal of X )

A2: for x, y being Element of X st x \ y in I holds

x \ (y \ (y \ x)) in I

x \ y in I

( I is commutative Ideal of X & I is positive-implicative-ideal of X )

let I be Ideal of X; :: thesis: ( I is implicative-ideal of X implies ( I is commutative Ideal of X & I is positive-implicative-ideal of X ) )

assume A1: I is implicative-ideal of X ; :: thesis: ( I is commutative Ideal of X & I is positive-implicative-ideal of X )

A2: for x, y being Element of X st x \ y in I holds

x \ (y \ (y \ x)) in I

proof

for x, y being Element of X st (x \ y) \ y in I holds
let x, y be Element of X; :: thesis: ( x \ y in I implies x \ (y \ (y \ x)) in I )

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

.= (y \ (y \ x)) ` by BCIALG_1:def 5

.= 0. X by BCIALG_1:def 8 ;

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

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

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

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

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

then ((x \ (y \ (y \ x))) \ (y \ (x \ (y \ (y \ x))))) \ (x \ y) <= 0. X by A3, BCIALG_1:def 3;

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

then ((x \ (y \ (y \ x))) \ (y \ (x \ (y \ (y \ x))))) \ (x \ y) = 0. X by BCIALG_1:2;

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

assume x \ y in I ; :: thesis: x \ (y \ (y \ x)) in I

hence x \ (y \ (y \ x)) in I by A1, A4, Th5, Th50; :: thesis: verum

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

.= (y \ (y \ x)) ` by BCIALG_1:def 5

.= 0. X by BCIALG_1:def 8 ;

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

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

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

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

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

then ((x \ (y \ (y \ x))) \ (y \ (x \ (y \ (y \ x))))) \ (x \ y) <= 0. X by A3, BCIALG_1:def 3;

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

then ((x \ (y \ (y \ x))) \ (y \ (x \ (y \ (y \ x))))) \ (x \ y) = 0. X by BCIALG_1:2;

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

assume x \ y in I ; :: thesis: x \ (y \ (y \ x)) in I

hence x \ (y \ (y \ x)) in I by A1, A4, Th5, Th50; :: thesis: verum

x \ y in I

proof

hence
( I is commutative Ideal of X & I is positive-implicative-ideal of X )
by A2, Th33, Th51; :: thesis: verum
let x, y be Element of X; :: thesis: ( (x \ y) \ y in I implies x \ y in I )

((x \ y) \ (x \ (x \ y))) \ ((x \ y) \ y) = 0. X by BCIALG_1:1;

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

assume (x \ y) \ y in I ; :: thesis: x \ y in I

hence x \ y in I by A1, A5, Th5, Th50; :: thesis: verum

end;((x \ y) \ (x \ (x \ y))) \ ((x \ y) \ y) = 0. X by BCIALG_1:1;

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

assume (x \ y) \ y in I ; :: thesis: x \ y in I

hence x \ y in I by A1, A5, Th5, Th50; :: thesis: verum