let X be BCK-algebra; :: thesis: for IT being non empty Subset of X st IT is Commutative-Ideal of X holds
for x, y being Element of X st x \ (x \ y) in IT holds
(y \ (y \ x)) \ (x \ y) in IT
let IT be non empty Subset of X; :: thesis: ( IT is Commutative-Ideal of X implies for x, y being Element of X st x \ (x \ y) in IT holds
(y \ (y \ x)) \ (x \ y) in IT )
assume IT is Commutative-Ideal of X ; :: thesis: for x, y being Element of X st x \ (x \ y) in IT holds
(y \ (y \ x)) \ (x \ y) in IT
then A1: IT is Ideal of X by Th26;
let x, y be Element of X; :: thesis: ( x \ (x \ y) in IT implies (y \ (y \ x)) \ (x \ y) in IT )
((y \ (y \ x)) \ (x \ y)) \ (x \ (x \ y)) = ((y \ (x \ y)) \ (y \ x)) \ (x \ (x \ y)) by BCIALG_1:7
.= 0. X by BCIALG_1:11 ;
then A2: (y \ (y \ x)) \ (x \ y) <= x \ (x \ y) ;
assume x \ (x \ y) in IT ; :: thesis: (y \ (y \ x)) \ (x \ y) in IT
hence (y \ (y \ x)) \ (x \ y) in IT by A1, A2, BCIALG_1:46; :: thesis: verum