let X be BCK-algebra; :: thesis: for I being Ideal of X
for x, y being Element of X st x \ (x \ y) in I holds
( x \ ((x \ y) \ ((x \ y) \ x)) in I & (y \ (y \ x)) \ x in I & (y \ (y \ x)) \ (x \ y) in I )
let I be Ideal of X; :: thesis: for x, y being Element of X st x \ (x \ y) in I holds
( x \ ((x \ y) \ ((x \ y) \ x)) in I & (y \ (y \ x)) \ x in I & (y \ (y \ x)) \ (x \ y) in I )
let x, y be Element of X; :: thesis: ( x \ (x \ y) in I implies ( x \ ((x \ y) \ ((x \ y) \ x)) in I & (y \ (y \ x)) \ x in I & (y \ (y \ x)) \ (x \ y) in I ) )
assume A1: x \ (x \ y) in I ; :: thesis: ( x \ ((x \ y) \ ((x \ y) \ x)) in I & (y \ (y \ x)) \ x in I & (y \ (y \ x)) \ (x \ y) in I )
(x \ y) \ ((x \ y) \ x) = (x \ y) \ ((x \ x) \ y) by BCIALG_1:7
.= (x \ ((x \ x) \ y)) \ y by BCIALG_1:7
.= (x \ (y `)) \ y by BCIALG_1:def 5
.= (x \ (0. X)) \ y by BCIALG_1:def 8
.= x \ y by BCIALG_1:2 ;
hence x \ ((x \ y) \ ((x \ y) \ x)) in I by A1; :: thesis: ( (y \ (y \ x)) \ x in I & (y \ (y \ x)) \ (x \ y) in I )
((y \ (0. X)) \ (y \ x)) \ (x \ (0. X)) = 0. X by BCIALG_1:1;
then ((y \ (0. X)) \ (y \ x)) \ (x \ (0. X)) in I by BCIALG_1:def 18;
then (y \ (y \ x)) \ (x \ (0. X)) in I by BCIALG_1:2;
hence (y \ (y \ x)) \ x in I by BCIALG_1:2; :: thesis: (y \ (y \ x)) \ (x \ y) in I
((y \ (0. X)) \ (y \ x)) \ (x \ (0. X)) = 0. X by BCIALG_1:1;
then (y \ (0. X)) \ (y \ x) <= x \ (0. X) ;
then ((y \ (0. X)) \ (y \ x)) \ (x \ y) <= (x \ (0. X)) \ (x \ y) by BCIALG_1:5;
then (y \ (y \ x)) \ (x \ y) <= (x \ (0. X)) \ (x \ y) by BCIALG_1:2;
then (y \ (y \ x)) \ (x \ y) <= x \ (x \ y) by BCIALG_1:2;
then ((y \ (y \ x)) \ (x \ y)) \ (x \ (x \ y)) = 0. X ;
then ((y \ (y \ x)) \ (x \ y)) \ (x \ (x \ y)) in I by BCIALG_1:def 18;
hence (y \ (y \ x)) \ (x \ y) in I by A1, BCIALG_1:def 18; :: thesis: verum