:: BCIIDEAL semantic presentation

begin


theorem :: BCIIDEAL:1
for X being BCI-algebra
for x, y, z, u being Element of X st x <= y holds
u \ (z \ x) <= u \ (z \ y)
proof
let X be BCI-algebra; ::_thesis: for x, y, z, u being Element of X st x <= y holds
u \ (z \ x) <= u \ (z \ y)
let x, y, z, u be Element of X; ::_thesis: ( x <= y implies u \ (z \ x) <= u \ (z \ y) )
assume  x <= y ; ::_thesis: u \ (z \ x) <= u \ (z \ y)
then  z \ y <= z \ x by BCIALG_1:5;
hence  u \ (z \ x) <= u \ (z \ y) by BCIALG_1:5; ::_thesis: verum
end;

theorem :: BCIIDEAL:2
for X being BCI-algebra
for x, y, z, u being Element of X holds (x \ (y \ z)) \ (x \ (y \ u)) <= z \ u
proof
let X be BCI-algebra; ::_thesis: for x, y, z, u being Element of X holds (x \ (y \ z)) \ (x \ (y \ u)) <= z \ u
let x, y, z, u be Element of X; ::_thesis: (x \ (y \ z)) \ (x \ (y \ u)) <= z \ u
 ((x \ (y \ z)) \ (x \ (y \ u))) \ ((y \ u) \ (y \ z)) = 0. X by BCIALG_1:1;
then  (x \ (y \ z)) \ (x \ (y \ u)) <= (y \ u) \ (y \ z) by BCIALG_1:def_11;
then A1: ((x \ (y \ z)) \ (x \ (y \ u))) \ (z \ u) <= ((y \ u) \ (y \ z)) \ (z \ u) by BCIALG_1:5;
 ((y \ u) \ (y \ z)) \ (z \ u) = ((y \ u) \ (z \ u)) \ (y \ z) by BCIALG_1:7;
then  ((x \ (y \ z)) \ (x \ (y \ u))) \ (z \ u) <= 0. X by A1, BCIALG_1:def_3;
then  (((x \ (y \ z)) \ (x \ (y \ u))) \ (z \ u)) \ (0. X) = 0. X by BCIALG_1:def_11;
then  ((x \ (y \ z)) \ (x \ (y \ u))) \ (z \ u) = 0. X by BCIALG_1:2;
hence  (x \ (y \ z)) \ (x \ (y \ u)) <= z \ u by BCIALG_1:def_11; ::_thesis: verum
end;

theorem :: BCIIDEAL:3
for X being BCI-algebra
for x, y, z, u, v being Element of X holds (x \ (y \ (z \ u))) \ (x \ (y \ (z \ v))) <= v \ u
proof
let X be BCI-algebra; ::_thesis: for x, y, z, u, v being Element of X holds (x \ (y \ (z \ u))) \ (x \ (y \ (z \ v))) <= v \ u
let x, y, z, u, v be Element of X; ::_thesis: (x \ (y \ (z \ u))) \ (x \ (y \ (z \ v))) <= v \ u
 ((x \ (y \ (z \ u))) \ (x \ (y \ (z \ v)))) \ ((y \ (z \ v)) \ (y \ (z \ u))) = 0. X by BCIALG_1:1;
then  (x \ (y \ (z \ u))) \ (x \ (y \ (z \ v))) <= (y \ (z \ v)) \ (y \ (z \ u)) by BCIALG_1:def_11;
then A1: ((x \ (y \ (z \ u))) \ (x \ (y \ (z \ v)))) \ ((z \ u) \ (z \ v)) <= ((y \ (z \ v)) \ (y \ (z \ u))) \ ((z \ u) \ (z \ v)) by BCIALG_1:5;
 ((y \ (z \ v)) \ (y \ (z \ u))) \ ((z \ u) \ (z \ v)) = ((y \ (z \ v)) \ ((z \ u) \ (z \ v))) \ (y \ (z \ u)) by BCIALG_1:7;
then  ((x \ (y \ (z \ u))) \ (x \ (y \ (z \ v)))) \ ((z \ u) \ (z \ v)) <= 0. X by A1, BCIALG_1:def_3;
then  (((x \ (y \ (z \ u))) \ (x \ (y \ (z \ v)))) \ ((z \ u) \ (z \ v))) \ (0. X) = 0. X by BCIALG_1:def_11;
then  ((x \ (y \ (z \ u))) \ (x \ (y \ (z \ v)))) \ ((z \ u) \ (z \ v)) = 0. X by BCIALG_1:2;
then  (x \ (y \ (z \ u))) \ (x \ (y \ (z \ v))) <= (z \ u) \ (z \ v) by BCIALG_1:def_11;
then A2: ((x \ (y \ (z \ u))) \ (x \ (y \ (z \ v)))) \ (v \ u) <= ((z \ u) \ (z \ v)) \ (v \ u) by BCIALG_1:5;
((z \ u) \ (z \ v)) \ (v \ u) = ((z \ u) \ (v \ u)) \ (z \ v) by BCIALG_1:7
.= 0. X by BCIALG_1:def_3 ;
then  (((x \ (y \ (z \ u))) \ (x \ (y \ (z \ v)))) \ (v \ u)) \ (0. X) = 0. X by A2, BCIALG_1:def_11;
then  ((x \ (y \ (z \ u))) \ (x \ (y \ (z \ v)))) \ (v \ u) = 0. X by BCIALG_1:2;
hence  (x \ (y \ (z \ u))) \ (x \ (y \ (z \ v))) <= v \ u by BCIALG_1:def_11; ::_thesis: verum
end;

theorem :: BCIIDEAL:4
for X being BCI-algebra
for x, y being Element of X holds ((0. X) \ (x \ y)) \ (y \ x) = 0. X
proof
let X be BCI-algebra; ::_thesis: for x, y being Element of X holds ((0. X) \ (x \ y)) \ (y \ x) = 0. X
let x, y be Element of X; ::_thesis: ((0. X) \ (x \ y)) \ (y \ x) = 0. X
 (((0. X) \ x) \ ((0. X) \ y)) \ (y \ x) = (((0. X) \ x) \ (y \ x)) \ ((0. X) \ y) by BCIALG_1:7;
then A1: (((0. X) \ x) \ ((0. X) \ y)) \ (y \ x) = (((y \ x) `) \ x) \ ((0. X) \ y) by BCIALG_1:7
.= (((y `) \ (x `)) \ x) \ ((0. X) \ y) by BCIALG_1:9
.= (((y `) \ x) \ (x `)) \ ((0. X) \ y) by BCIALG_1:7
.= (((y `) \ x) \ (y `)) \ (x `) by BCIALG_1:7
.= (((y `) \ (y `)) \ x) \ (x `) by BCIALG_1:7
.= (x `) \ (x `) by BCIALG_1:def_5
.= 0. X by BCIALG_1:def_5 ;
((0. X) \ (x \ y)) \ (y \ x) = ((x \ y) `) \ (y \ x)
.= ((x `) \ (y `)) \ (y \ x) by BCIALG_1:9
.= (((0. X) \ x) \ ((0. X) \ y)) \ (y \ x) ;
hence  ((0. X) \ (x \ y)) \ (y \ x) = 0. X by A1; ::_thesis: verum
end;

definition
let X be BCI-algebra;
let a be Element of X;
func initial_section a ->  set  equals :: BCIIDEAL:def 1
 {  x where x is Element of X : x <= a  }  ;
coherence
  {  x where x is Element of X : x <= a  }  is set ;
end;

:: deftheorem  defines initial_section BCIIDEAL:def_1_:_
 for X being BCI-algebra
for a being Element of X holds initial_section a =  {  x where x is Element of X : x <= a  }  ;

theorem Th5: :: BCIIDEAL:5
for X being BCI-algebra
for A being Ideal of X
for x being Element of X
for a being Element of A st x <= a holds
x in A
proof
let X be BCI-algebra; ::_thesis: for A being Ideal of X
for x being Element of X
for a being Element of A st x <= a holds
x in A
let A be Ideal of X; ::_thesis: for x being Element of X
for a being Element of A st x <= a holds
x in A
let x be Element of X; ::_thesis: for a being Element of A st x <= a holds
x in A
let a be Element of A; ::_thesis: ( x <= a implies x in A )
assume  x <= a ; ::_thesis: x in A
then  x \ a = 0. X by BCIALG_1:def_11;
then  x \ a in A by BCIALG_1:def_18;
hence  x in A by BCIALG_1:def_18; ::_thesis: verum
end;

theorem :: BCIIDEAL:6
for X being BCI-algebra
for x, a, b being Element of AtomSet X st x is Element of BranchV b holds
a \ x = a \ b
proof
let X be BCI-algebra; ::_thesis: for x, a, b being Element of AtomSet X st x is Element of BranchV b holds
a \ x = a \ b
set P = AtomSet X;
let x, a, b be Element of AtomSet X; ::_thesis: ( x is Element of BranchV b implies a \ x = a \ b )
set B = BranchV b;
assume  x is Element of BranchV b ; ::_thesis: a \ x = a \ b
then  x in BranchV b ;
then  ex x3 being Element of X st
( x = x3 & b <= x3 ) ;
then A1: b \ x = 0. X by BCIALG_1:def_11;
 x in  {  x1 where x1 is Element of X : x1 is minimal  }  ;
then  ex x1 being Element of X st
( x = x1 & x1 is minimal ) ;
hence  a \ x = a \ b by A1, BCIALG_1:def_14; ::_thesis: verum
end;

theorem :: BCIIDEAL:7
for X being BCI-algebra
for a being Element of X
for x, b being Element of AtomSet X st x is Element of BranchV b holds
a \ x = a \ b
proof
let X be BCI-algebra; ::_thesis: for a being Element of X
for x, b being Element of AtomSet X st x is Element of BranchV b holds
a \ x = a \ b
set P = AtomSet X;
let a be Element of X; ::_thesis: for x, b being Element of AtomSet X st x is Element of BranchV b holds
a \ x = a \ b
let x, b be Element of AtomSet X; ::_thesis: ( x is Element of BranchV b implies a \ x = a \ b )
set B = BranchV b;
assume  x is Element of BranchV b ; ::_thesis: a \ x = a \ b
then  x in BranchV b ;
then  ex x3 being Element of X st
( x = x3 & b <= x3 ) ;
then A1: b \ x = 0. X by BCIALG_1:def_11;
 x in  {  x1 where x1 is Element of X : x1 is minimal  }  ;
then  ex x1 being Element of X st
( x = x1 & x1 is minimal ) ;
hence  a \ x = a \ b by A1, BCIALG_1:def_14; ::_thesis: verum
end;

theorem :: BCIIDEAL:8
for X being BCI-algebra
for A being Ideal of X
for a being Element of A holds initial_section a c= A
proof
let X be BCI-algebra; ::_thesis: for A being Ideal of X
for a being Element of A holds initial_section a c= A
let A be Ideal of X; ::_thesis: for a being Element of A holds initial_section a c= A
let a be Element of A; ::_thesis: initial_section a c= A
let b be set ; :: according to TARSKI:def_3 ::_thesis: ( not b in initial_section a or b in A )
assume  b in initial_section a ; ::_thesis: b in A
then  ex x1 being Element of X st
( b = x1 & x1 <= a ) ;
hence  b in A by Th5; ::_thesis: verum
end;

theorem :: BCIIDEAL:9
for X being BCI-algebra st AtomSet X is Ideal of X holds
for x being Element of BCK-part X
for a being Element of AtomSet X st x \ a in AtomSet X holds
x = 0. X
proof
let X be BCI-algebra; ::_thesis: ( AtomSet X is Ideal of X implies for x being Element of BCK-part X
for a being Element of AtomSet X st x \ a in AtomSet X holds
x = 0. X )
set B = BCK-part X;
set P = AtomSet X;
A1: for x being Element of X holds
( x in {(0. X)} iff x in (BCK-part X) /\ (AtomSet X) )
proof
let x be Element of X; ::_thesis: ( x in {(0. X)} iff x in (BCK-part X) /\ (AtomSet X) )
 ( 0. X in BCK-part X & 0. X in AtomSet X ) by BCIALG_1:19;
then  0. X in (BCK-part X) /\ (AtomSet X) by XBOOLE_0:def_4;
hence  ( x in {(0. X)} implies x in (BCK-part X) /\ (AtomSet X) ) by TARSKI:def_1; ::_thesis: ( x in (BCK-part X) /\ (AtomSet X) implies x in {(0. X)} )
thus  ( x in (BCK-part X) /\ (AtomSet X) implies x in {(0. X)} ) ::_thesis: verum
proof
assume A2: x in (BCK-part X) /\ (AtomSet X) ; ::_thesis: x in {(0. X)}
then  x in BCK-part X by XBOOLE_0:def_4;
then  ex x1 being Element of X st
( x = x1 & 0. X <= x1 ) ;
then A3: (0. X) \ x = 0. X by BCIALG_1:def_11;
 x in  {  x2 where x2 is Element of X : x2 is minimal  }  by A2, XBOOLE_0:def_4;
then  ex x2 being Element of X st
( x = x2 & x2 is minimal ) ;
then  0. X = x by A3, BCIALG_1:def_14;
hence  x in {(0. X)} by TARSKI:def_1; ::_thesis: verum
end;
end;
assume A4: AtomSet X is Ideal of X ; ::_thesis: for x being Element of BCK-part X
for a being Element of AtomSet X st x \ a in AtomSet X holds
x = 0. X
 for x being Element of BCK-part X
for a being Element of AtomSet X st x \ a in AtomSet X holds
x = 0. X
proof
let x be Element of BCK-part X; ::_thesis: for a being Element of AtomSet X st x \ a in AtomSet X holds
x = 0. X
let a be Element of AtomSet X; ::_thesis: ( x \ a in AtomSet X implies x = 0. X )
assume  x \ a in AtomSet X ; ::_thesis: x = 0. X
then  x in AtomSet X by A4, BCIALG_1:def_18;
then  x in (BCK-part X) /\ (AtomSet X) by XBOOLE_0:def_4;
then  x in {(0. X)} by A1;
hence  x = 0. X by TARSKI:def_1; ::_thesis: verum
end;
hence  for x being Element of BCK-part X
for a being Element of AtomSet X st x \ a in AtomSet X holds
x = 0. X ; ::_thesis: verum
end;

theorem :: BCIIDEAL:10
for X being BCI-algebra st AtomSet X is Ideal of X holds
AtomSet X is closed Ideal of X
proof
let X be BCI-algebra; ::_thesis: ( AtomSet X is Ideal of X implies AtomSet X is closed Ideal of X )
set P = AtomSet X;
A1: for x being Element of AtomSet X holds x ` in AtomSet X
proof
let x be Element of AtomSet X; ::_thesis: x ` in AtomSet X
 x ` is minimal by BCIALG_2:30;
hence  x ` in AtomSet X ; ::_thesis: verum
end;
assume  AtomSet X is Ideal of X ; ::_thesis: AtomSet X is closed Ideal of X
hence  AtomSet X is closed Ideal of X by A1, BCIALG_1:def_19; ::_thesis: verum
end;

definition
let X be BCI-algebra;
let I be Ideal of X;
attrI is positive  means :: BCIIDEAL:def 2
 for x being Element of I holds x is positive ;
end;

:: deftheorem  defines positive BCIIDEAL:def_2_:_
 for X being BCI-algebra
for I being Ideal of X holds
( I is positive iff for x being Element of I holds x is positive );

theorem :: BCIIDEAL:11
for X being BCK-algebra
for A, I being Ideal of X holds
( A /\ I = {(0. X)} iff for x being Element of A
for y being Element of I holds x \ y = x )
proof
let X be BCK-algebra; ::_thesis: for A, I being Ideal of X holds
( A /\ I = {(0. X)} iff for x being Element of A
for y being Element of I holds x \ y = x )
let A, I be Ideal of X; ::_thesis: ( A /\ I = {(0. X)} iff for x being Element of A
for y being Element of I holds x \ y = x )
thus  ( A /\ I = {(0. X)} implies for x being Element of A
for y being Element of I holds x \ y = x ) ::_thesis: ( ( for x being Element of A
for y being Element of I holds x \ y = x ) implies A /\ I = {(0. X)} )
proof
assume A1: A /\ I = {(0. X)} ; ::_thesis: for x being Element of A
for y being Element of I holds x \ y = x
let x be Element of A; ::_thesis: for y being Element of I holds x \ y = x
let y be Element of I; ::_thesis: x \ y = x
 (x \ (x \ y)) \ y = 0. X by BCIALG_1:1;
then  x \ (x \ y) <= y by BCIALG_1:def_11;
then A2: x \ (x \ y) in I by Th5;
(x \ (x \ y)) \ x = (x \ x) \ (x \ y) by BCIALG_1:7
.= (x \ y) ` by BCIALG_1:def_5
.= 0. X by BCIALG_1:def_8 ;
then  x \ (x \ y) <= x by BCIALG_1:def_11;
then  x \ (x \ y) in A by Th5;
then  x \ (x \ y) in {(0. X)} by A1, A2, XBOOLE_0:def_4;
then A3: x \ (x \ y) = 0. X by TARSKI:def_1;
(x \ y) \ x = (x \ x) \ y by BCIALG_1:7
.= y ` by BCIALG_1:def_5
.= 0. X by BCIALG_1:def_8 ;
hence  x \ y = x by A3, BCIALG_1:def_7; ::_thesis: verum
end;
thus  ( ( for x being Element of A
for y being Element of I holds x \ y = x ) implies A /\ I = {(0. X)} ) ::_thesis: verum
proof
assume A4: for x being Element of A
for y being Element of I holds x \ y = x ; ::_thesis: A /\ I = {(0. X)}
thus  A /\ I c= {(0. X)} :: according to XBOOLE_0:def_10 ::_thesis: {(0. X)} c= A /\ I
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A /\ I or x in {(0. X)} )
assume A5: x in A /\ I ; ::_thesis: x in {(0. X)}
then reconsider xxx = x as Element of A by XBOOLE_0:def_4;
reconsider xx = x as Element of I by A5, XBOOLE_0:def_4;
 xxx \ xx = xxx by A4;
then  x = 0. X by BCIALG_1:def_5;
hence  x in {(0. X)} by TARSKI:def_1; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {(0. X)} or x in A /\ I )
assume  x in {(0. X)} ; ::_thesis: x in A /\ I
then A6: x = 0. X by TARSKI:def_1;
 ( 0. X in A & 0. X in I ) by BCIALG_1:def_18;
hence  x in A /\ I by A6, XBOOLE_0:def_4; ::_thesis: verum
end;
end;

theorem :: BCIIDEAL:12
for X being associative BCI-algebra
for A being Ideal of X holds A is closed
proof
let X be associative BCI-algebra; ::_thesis: for A being Ideal of X holds A is closed
let A be Ideal of X; ::_thesis: A is closed
 for x being Element of A holds x ` in A
proof
let x be Element of A; ::_thesis: x ` in A
(0. X) \ x = x \ (0. X) by BCIALG_1:48
.= x by BCIALG_1:2 ;
hence  x ` in A ; ::_thesis: verum
end;
hence  A is closed by BCIALG_1:def_19; ::_thesis: verum
end;

theorem :: BCIIDEAL:13
for X being BCI-algebra
for A being Ideal of X st X is quasi-associative holds
A is closed
proof
let X be BCI-algebra; ::_thesis: for A being Ideal of X st X is quasi-associative holds
A is closed
let A be Ideal of X; ::_thesis: ( X is quasi-associative implies A is closed )
assume A1: X is quasi-associative ; ::_thesis: A is closed
 for x being Element of A holds x ` in A
proof
let x be Element of A; ::_thesis: x ` in A
 x ` <= x by A1, BCIALG_1:71;
hence  x ` in A by Th5; ::_thesis: verum
end;
hence  A is closed by BCIALG_1:def_19; ::_thesis: verum
end;

begin

definition
let X be BCI-algebra;
let IT be Ideal of X;
attrIT is associative  means :Def3: :: BCIIDEAL:def 3
( 0. X in IT & ( for x, y, z being Element of X st x \ (y \ z) in IT & y \ z in IT holds
x in IT ) );
end;

:: deftheorem Def3 defines associative BCIIDEAL:def_3_:_
 for X being BCI-algebra
for IT being Ideal of X holds
( IT is associative iff ( 0. X in IT & ( for x, y, z being Element of X st x \ (y \ z) in IT & y \ z in IT holds
x in IT ) ) );

registration
let X be BCI-algebra;
cluster non empty associative for Ideal of X;
existence
 ex b1 being Ideal of X st b1 is associative
proof
take Y = {(0. X)}; ::_thesis: ( Y is Element of K19( the carrier of X) & Y is Ideal of X & Y is associative )
reconsider YY = Y as Ideal of X by BCIALG_1:43;
A1: 0. X in YY by TARSKI:def_1;
 for x, y, z being Element of X st x \ (y \ z) in YY & y \ z in YY holds
x = 0. X
proof
let x, y, z be Element of X; ::_thesis: ( x \ (y \ z) in YY & y \ z in YY implies x = 0. X )
assume  ( x \ (y \ z) in YY & y \ z in YY ) ; ::_thesis: x = 0. X
then  ( x \ (y \ z) = 0. X & y \ z = 0. X ) by TARSKI:def_1;
hence  x = 0. X by BCIALG_1:2; ::_thesis: verum
end;
then  for x, y, z being Element of X st x \ (y \ z) in YY & y \ z in YY holds
x in YY by A1;
hence  ( Y is Element of K19( the carrier of X) & Y is Ideal of X & Y is associative ) by A1, Def3; ::_thesis: verum
end;
end;

definition
let X be BCI-algebra;
mode associative-ideal of X ->  non empty Subset of X means :Def4: :: BCIIDEAL:def 4
( 0. X in it & ( for x, y, z being Element of X st (x \ y) \ z in it & y \ z in it holds
x in it ) );
existence
 ex b1 being non empty Subset of X st
( 0. X in b1 & ( for x, y, z being Element of X st (x \ y) \ z in b1 & y \ z in b1 holds
x in b1 ) )
proof
take X1 = the carrier of X; ::_thesis: ( X1 is non empty Subset of X & 0. X in X1 & ( for x, y, z being Element of X st (x \ y) \ z in X1 & y \ z in X1 holds
x in X1 ) )
 X1 c= the carrier of X ;
hence  ( X1 is non empty Subset of X & 0. X in X1 & ( for x, y, z being Element of X st (x \ y) \ z in X1 & y \ z in X1 holds
x in X1 ) ) ; ::_thesis: verum
end;
end;

:: deftheorem Def4 defines associative-ideal BCIIDEAL:def_4_:_
 for X being BCI-algebra
for b2 being non empty Subset of X holds
( b2 is associative-ideal of X iff ( 0. X in b2 & ( for x, y, z being Element of X st (x \ y) \ z in b2 & y \ z in b2 holds
x in b2 ) ) );

theorem :: BCIIDEAL:14
for X being BCI-algebra
for X1 being non empty Subset of X st X1 is associative-ideal of X holds
X1 is Ideal of X
proof
let X be BCI-algebra; ::_thesis: for X1 being non empty Subset of X st X1 is associative-ideal of X holds
X1 is Ideal of X
let X1 be non empty Subset of X; ::_thesis: ( X1 is associative-ideal of X implies X1 is Ideal of X )
assume A1: X1 is associative-ideal of X ; ::_thesis: X1 is Ideal of X
A2: for x, y being Element of X st x \ y in X1 & y in X1 holds
x in X1
proof
let x, y be Element of X; ::_thesis: ( x \ y in X1 & y in X1 implies x in X1 )
assume  ( x \ y in X1 & y in X1 ) ; ::_thesis: x in X1
then  ( (x \ y) \ (0. X) in X1 & y \ (0. X) in X1 ) by BCIALG_1:2;
hence  x in X1 by A1, Def4; ::_thesis: verum
end;
 0. X in X1 by A1, Def4;
hence  X1 is Ideal of X by A2, BCIALG_1:def_18; ::_thesis: verum
end;

theorem Th15: :: BCIIDEAL:15
for X being BCI-algebra
for I being Ideal of X holds
( I is associative-ideal of X iff for x, y, z being Element of X st (x \ y) \ z in I holds
x \ (y \ z) in I )
proof
let X be BCI-algebra; ::_thesis: for I being Ideal of X holds
( I is associative-ideal of X iff for x, y, z being Element of X st (x \ y) \ z in I holds
x \ (y \ z) in I )
let I be Ideal of X; ::_thesis: ( I is associative-ideal of X iff for x, y, z being Element of X st (x \ y) \ z in I holds
x \ (y \ z) in I )
thus  ( I is associative-ideal of X implies for x, y, z being Element of X st (x \ y) \ z in I holds
x \ (y \ z) in I ) ::_thesis: ( ( for x, y, z being Element of X st (x \ y) \ z in I holds
x \ (y \ z) in I ) implies I is associative-ideal of X )
proof
assume A1: I is associative-ideal of X ; ::_thesis: for x, y, z being Element of X st (x \ y) \ z in I holds
x \ (y \ z) in I
let x, y, z be Element of X; ::_thesis: ( (x \ y) \ z in I implies x \ (y \ z) in I )
assume A2: (x \ y) \ z in I ; ::_thesis: x \ (y \ z) in I
 (x \ (x \ y)) \ y = 0. X by BCIALG_1:1;
then  x \ (x \ y) <= y by BCIALG_1:def_11;
then  (x \ (x \ y)) \ (y \ z) <= y \ (y \ z) by BCIALG_1:5;
then A3: ((x \ (x \ y)) \ (y \ z)) \ z <= (y \ (y \ z)) \ z by BCIALG_1:5;
 (y \ (y \ z)) \ z = 0. X by BCIALG_1:1;
then  (((x \ (x \ y)) \ (y \ z)) \ z) \ (0. X) = 0. X by A3, BCIALG_1:def_11;
then  ((x \ (x \ y)) \ (y \ z)) \ z = 0. X by BCIALG_1:2;
then  ((x \ (x \ y)) \ (y \ z)) \ z in I by A1, Def4;
then  ((x \ (y \ z)) \ (x \ y)) \ z in I by BCIALG_1:7;
hence  x \ (y \ z) in I by A1, A2, Def4; ::_thesis: verum
end;
assume A4: for x, y, z being Element of X st (x \ y) \ z in I holds
x \ (y \ z) in I ; ::_thesis: I is associative-ideal of X
A5: for x, y, z being Element of X st (x \ y) \ z in I & y \ z in I holds
x in I
proof
let x, y, z be Element of X; ::_thesis: ( (x \ y) \ z in I & y \ z in I implies x in I )
assume that
A6: (x \ y) \ z in I and
A7: y \ z in I ; ::_thesis: x in I
 x \ (y \ z) in I by A4, A6;
hence  x in I by A7, BCIALG_1:def_18; ::_thesis: verum
end;
 0. X in I by BCIALG_1:def_18;
hence  I is associative-ideal of X by A5, Def4; ::_thesis: verum
end;

theorem :: BCIIDEAL:16
for X being BCI-algebra
for I being Ideal of X st I is associative-ideal of X holds
for x being Element of X holds x \ ((0. X) \ x) in I
proof
let X be BCI-algebra; ::_thesis: for I being Ideal of X st I is associative-ideal of X holds
for x being Element of X holds x \ ((0. X) \ x) in I
let I be Ideal of X; ::_thesis: ( I is associative-ideal of X implies for x being Element of X holds x \ ((0. X) \ x) in I )
assume A1: I is associative-ideal of X ; ::_thesis: for x being Element of X holds x \ ((0. X) \ x) in I
let x be Element of X; ::_thesis: x \ ((0. X) \ x) in I
 x \ x = 0. X by BCIALG_1:def_5;
then A2: (x \ (0. X)) \ x = 0. X by BCIALG_1:2;
 0. X in I by A1, Def4;
hence  x \ ((0. X) \ x) in I by A1, A2, Th15; ::_thesis: verum
end;

theorem :: BCIIDEAL:17
for X being BCI-algebra
for I being Ideal of X st ( for x being Element of X holds x \ ((0. X) \ x) in I ) holds
I is closed Ideal of X
proof
let X be BCI-algebra; ::_thesis: for I being Ideal of X st ( for x being Element of X holds x \ ((0. X) \ x) in I ) holds
I is closed Ideal of X
let I be Ideal of X; ::_thesis: ( ( for x being Element of X holds x \ ((0. X) \ x) in I ) implies I is closed Ideal of X )
assume A1: for x being Element of X holds x \ ((0. X) \ x) in I ; ::_thesis: I is closed Ideal of X
 for x1 being Element of I holds x1 ` in I
proof
let x1 be Element of I; ::_thesis: x1 ` in I
 ((0. X) \ x1) \ x1 = ((0. X) \ ((0. X) \ ((0. X) \ x1))) \ x1 by BCIALG_1:8;
then  ((0. X) \ x1) \ x1 = ((0. X) \ x1) \ ((0. X) \ ((0. X) \ x1)) by BCIALG_1:7;
then  ((0. X) \ x1) \ x1 in I by A1;
hence  x1 ` in I by BCIALG_1:def_18; ::_thesis: verum
end;
hence  I is closed Ideal of X by BCIALG_1:def_19; ::_thesis: verum
end;

definition
let X be BCI-algebra;
mode p-ideal of X ->  non empty Subset of X means :Def5: :: BCIIDEAL:def 5
( 0. X in it & ( for x, y, z being Element of X st (x \ z) \ (y \ z) in it & y in it holds
x in it ) );
existence
 ex b1 being non empty Subset of X st
( 0. X in b1 & ( for x, y, z being Element of X st (x \ z) \ (y \ z) in b1 & y in b1 holds
x in b1 ) )
proof
take X1 = the carrier of X; ::_thesis: ( X1 is non empty Subset of X & 0. X in X1 & ( for x, y, z being Element of X st (x \ z) \ (y \ z) in X1 & y in X1 holds
x in X1 ) )
 X1 c= X1 ;
hence  ( X1 is non empty Subset of X & 0. X in X1 & ( for x, y, z being Element of X st (x \ z) \ (y \ z) in X1 & y in X1 holds
x in X1 ) ) ; ::_thesis: verum
end;
end;

:: deftheorem Def5 defines p-ideal BCIIDEAL:def_5_:_
 for X being BCI-algebra
for b2 being non empty Subset of X holds
( b2 is p-ideal of X iff ( 0. X in b2 & ( for x, y, z being Element of X st (x \ z) \ (y \ z) in b2 & y in b2 holds
x in b2 ) ) );

theorem :: BCIIDEAL:18
for X being BCI-algebra
for X1 being non empty Subset of X st X1 is p-ideal of X holds
X1 is Ideal of X
proof
let X be BCI-algebra; ::_thesis: for X1 being non empty Subset of X st X1 is p-ideal of X holds
X1 is Ideal of X
let X1 be non empty Subset of X; ::_thesis: ( X1 is p-ideal of X implies X1 is Ideal of X )
assume A1: X1 is p-ideal of X ; ::_thesis: X1 is Ideal of X
A2: for x, y being Element of X st x \ y in X1 & y in X1 holds
x in X1
proof
let x, y be Element of X; ::_thesis: ( x \ y in X1 & y in X1 implies x in X1 )
assume that
A3: x \ y in X1 and
A4: y in X1 ; ::_thesis: x in X1
 (x \ (0. X)) \ y in X1 by A3, BCIALG_1:2;
then  (x \ (0. X)) \ (y \ (0. X)) in X1 by BCIALG_1:2;
hence  x in X1 by A1, A4, Def5; ::_thesis: verum
end;
 0. X in X1 by A1, Def5;
hence  X1 is Ideal of X by A2, BCIALG_1:def_18; ::_thesis: verum
end;

theorem Th19: :: BCIIDEAL:19
for X being BCI-algebra
for I being Ideal of X st I is p-ideal of X holds
BCK-part X c= I
proof
let X be BCI-algebra; ::_thesis: for I being Ideal of X st I is p-ideal of X holds
BCK-part X c= I
let I be Ideal of X; ::_thesis: ( I is p-ideal of X implies BCK-part X c= I )
assume A1: I is p-ideal of X ; ::_thesis: BCK-part X c= I
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in BCK-part X or x in I )
assume A2: x in BCK-part X ; ::_thesis: x in I
then A3: ex x1 being Element of X st
( x = x1 & 0. X <= x1 ) ;
reconsider x = x as Element of X by A2;
 (0. X) \ x = 0. X by A3, BCIALG_1:def_11;
then  (0. X) \ ((0. X) \ x) = 0. X by BCIALG_1:2;
then A4: (x \ x) \ ((0. X) \ x) = 0. X by BCIALG_1:def_5;
 0. X in I by A1, Def5;
hence  x in I by A1, A4, Def5; ::_thesis: verum
end;

theorem :: BCIIDEAL:20
for X being BCI-algebra holds BCK-part X is p-ideal of X
proof
let X be BCI-algebra; ::_thesis: BCK-part X is p-ideal of X
set A = BCK-part X;
A1: now__::_thesis:_for_x,_y,_z_being_Element_of_X_st_(x_\_z)_\_(y_\_z)_in_BCK-part_X_&_y_in_BCK-part_X_holds_
x_in_BCK-part_X
let x, y, z be Element of X; ::_thesis: ( (x \ z) \ (y \ z) in BCK-part X & y in BCK-part X implies x in BCK-part X )
assume that
A2: (x \ z) \ (y \ z) in BCK-part X and
A3: y in BCK-part X ; ::_thesis: x in BCK-part X
 ex c being Element of X st
( (x \ z) \ (y \ z) = c & 0. X <= c ) by A2;
then  ((x \ z) \ (y \ z)) ` = 0. X by BCIALG_1:def_11;
then  ((x \ z) `) \ ((y \ z) `) = 0. X by BCIALG_1:9;
then A4: ((x `) \ (z `)) \ ((y \ z) `) = 0. X by BCIALG_1:9;
 ex d being Element of X st
( y = d & 0. X <= d ) by A3;
then  y ` = 0. X by BCIALG_1:def_11;
then  (((x `) \ (z `)) \ ((0. X) \ (z `))) \ ((x `) \ (0. X)) = ((x `) \ (0. X)) ` by A4, BCIALG_1:9;
then  (((x `) \ (z `)) \ ((0. X) \ (z `))) \ ((x `) \ (0. X)) = (x `) ` by BCIALG_1:2;
then  0. X = (0. X) \ ((0. X) \ x) by BCIALG_1:def_3;
then  (0. X) \ x = 0. X by BCIALG_1:1;
then  0. X <= x by BCIALG_1:def_11;
hence  x in BCK-part X ; ::_thesis: verum
end;
 (0. X) \ (0. X) = 0. X by BCIALG_1:def_5;
then  0. X <= 0. X by BCIALG_1:def_11;
then  0. X in BCK-part X ;
hence  BCK-part X is p-ideal of X by A1, Def5; ::_thesis: verum
end;

theorem Th21: :: BCIIDEAL:21
for X being BCI-algebra
for I being Ideal of X holds
( I is p-ideal of X iff for x, y being Element of X st x in I & x <= y holds
y in I )
proof
let X be BCI-algebra; ::_thesis: for I being Ideal of X holds
( I is p-ideal of X iff for x, y being Element of X st x in I & x <= y holds
y in I )
let I be Ideal of X; ::_thesis: ( I is p-ideal of X iff for x, y being Element of X st x in I & x <= y holds
y in I )
thus  ( I is p-ideal of X implies for x, y being Element of X st x in I & x <= y holds
y in I ) ::_thesis: ( ( for x, y being Element of X st x in I & x <= y holds
y in I ) implies I is p-ideal of X )
proof
assume  I is p-ideal of X ; ::_thesis: for x, y being Element of X st x in I & x <= y holds
y in I
then A1: BCK-part X c= I by Th19;
let x, y be Element of X; ::_thesis: ( x in I & x <= y implies y in I )
assume that
A2: x in I and
A3: x <= y ; ::_thesis: y in I
A4: x \ y = 0. X by A3, BCIALG_1:def_11;
then  (y \ x) ` = x \ y by BCIALG_1:6;
then  0. X <= y \ x by A4, BCIALG_1:def_11;
then  y \ x in BCK-part X ;
hence  y in I by A2, A1, BCIALG_1:def_18; ::_thesis: verum
end;
assume A5: for x, y being Element of X st x in I & x <= y holds
y in I ; ::_thesis: I is p-ideal of X
A6: for x, y, z being Element of X st (x \ z) \ (y \ z) in I & y in I holds
x in I
proof
let x, y, z be Element of X; ::_thesis: ( (x \ z) \ (y \ z) in I & y in I implies x in I )
assume that
A7: (x \ z) \ (y \ z) in I and
A8: y in I ; ::_thesis: x in I
 ((x \ z) \ (y \ z)) \ (x \ y) = 0. X by BCIALG_1:def_3;
then  (x \ z) \ (y \ z) <= x \ y by BCIALG_1:def_11;
then  x \ y in I by A5, A7;
hence  x in I by A8, BCIALG_1:def_18; ::_thesis: verum
end;
 0. X in I by BCIALG_1:def_18;
hence  I is p-ideal of X by A6, Def5; ::_thesis: verum
end;

theorem :: BCIIDEAL:22
for X being BCI-algebra
for I being Ideal of X holds
( I is p-ideal of X iff for x, y, z being Element of X st (x \ z) \ (y \ z) in I holds
x \ y in I )
proof
let X be BCI-algebra; ::_thesis: for I being Ideal of X holds
( I is p-ideal of X iff for x, y, z being Element of X st (x \ z) \ (y \ z) in I holds
x \ y in I )
let I be Ideal of X; ::_thesis: ( I is p-ideal of X iff for x, y, z being Element of X st (x \ z) \ (y \ z) in I holds
x \ y in I )
thus  ( I is p-ideal of X implies for x, y, z being Element of X st (x \ z) \ (y \ z) in I holds
x \ y in I ) ::_thesis: ( ( for x, y, z being Element of X st (x \ z) \ (y \ z) in I holds
x \ y in I ) implies I is p-ideal of X )
proof
assume A1: I is p-ideal of X ; ::_thesis: for x, y, z being Element of X st (x \ z) \ (y \ z) in I holds
x \ y in I
let x, y, z be Element of X; ::_thesis: ( (x \ z) \ (y \ z) in I implies x \ y in I )
assume A2: (x \ z) \ (y \ z) in I ; ::_thesis: x \ y in I
 ((x \ z) \ (y \ z)) \ (x \ y) = 0. X by BCIALG_1:def_3;
then  (x \ z) \ (y \ z) <= x \ y by BCIALG_1:def_11;
hence  x \ y in I by A1, A2, Th21; ::_thesis: verum
end;
assume A3: for x, y, z being Element of X st (x \ z) \ (y \ z) in I holds
x \ y in I ; ::_thesis: I is p-ideal of X
A4: for x, y, z being Element of X st (x \ z) \ (y \ z) in I & y in I holds
x in I
proof
let x, y, z be Element of X; ::_thesis: ( (x \ z) \ (y \ z) in I & y in I implies x in I )
assume that
A5: (x \ z) \ (y \ z) in I and
A6: y in I ; ::_thesis: x in I
 x \ y in I by A3, A5;
hence  x in I by A6, BCIALG_1:def_18; ::_thesis: verum
end;
 0. X in I by BCIALG_1:def_18;
hence  I is p-ideal of X by A4, Def5; ::_thesis: verum
end;

begin

definition
let X be BCK-algebra;
let IT be Ideal of X;
attrIT is commutative  means :Def6: :: BCIIDEAL:def 6
 for x, y, z being Element of X st (x \ y) \ z in IT & z in IT holds
x \ (y \ (y \ x)) in IT;
end;

:: deftheorem Def6 defines commutative BCIIDEAL:def_6_:_
 for X being BCK-algebra
for IT being Ideal of X holds
( IT is commutative iff for x, y, z being Element of X st (x \ y) \ z in IT & z in IT holds
x \ (y \ (y \ x)) in IT );

registration
let X be BCK-algebra;
cluster non empty commutative for Ideal of X;
existence
 ex b1 being Ideal of X st b1 is commutative
proof
set X1 = BCK-part X;
take  BCK-part X ; ::_thesis: ( BCK-part X is Ideal of X & BCK-part X is commutative )
A1: for x, y being Element of X st x \ y in BCK-part X & y in BCK-part X holds
x in BCK-part X
proof
let x, y be Element of X; ::_thesis: ( x \ y in BCK-part X & y in BCK-part X implies x in BCK-part X )
assume that
A2: x \ y in BCK-part X and
A3: y in BCK-part X ; ::_thesis: x in BCK-part X
 ex x2 being Element of X st
( y = x2 & 0. X <= x2 ) by A3;
then A4: y ` = 0. X by BCIALG_1:def_11;
 ex x1 being Element of X st
( x \ y = x1 & 0. X <= x1 ) by A2;
then  (x \ y) ` = 0. X by BCIALG_1:def_11;
then  (x `) \ (0. X) = 0. X by A4, BCIALG_1:9;
then  (0. X) \ x = 0. X by BCIALG_1:2;
then  0. X <= x by BCIALG_1:def_11;
hence  x in BCK-part X ; ::_thesis: verum
end;
A5: for x, y, z being Element of X st (x \ y) \ z in BCK-part X & z in BCK-part X holds
x \ (y \ (y \ x)) in BCK-part X
proof
let x, y, z be Element of X; ::_thesis: ( (x \ y) \ z in BCK-part X & z in BCK-part X implies x \ (y \ (y \ x)) in BCK-part X )
assume that
 (x \ y) \ z in BCK-part X and
 z in BCK-part X ; ::_thesis: x \ (y \ (y \ x)) in BCK-part X
(0. X) \ (x \ (y \ (y \ x))) = (x \ (y \ (y \ x))) `
.= 0. X by BCIALG_1:def_8 ;
then  0. X <= x \ (y \ (y \ x)) by BCIALG_1:def_11;
hence  x \ (y \ (y \ x)) in BCK-part X ; ::_thesis: verum
end;
 0. X in BCK-part X by BCIALG_1:19;
then  BCK-part X is Ideal of X by A1, BCIALG_1:def_18;
hence  ( BCK-part X is Ideal of X & BCK-part X is commutative ) by A5, Def6; ::_thesis: verum
end;
end;

theorem :: BCIIDEAL:23
for X being BCK-algebra holds BCK-part X is commutative Ideal of X
proof
let X be BCK-algebra; ::_thesis: BCK-part X is commutative Ideal of X
set B = BCK-part X;
A1: for x, y being Element of X st x \ y in BCK-part X & y in BCK-part X holds
x in BCK-part X
proof
let x, y be Element of X; ::_thesis: ( x \ y in BCK-part X & y in BCK-part X implies x in BCK-part X )
assume that
A2: x \ y in BCK-part X and
A3: y in BCK-part X ; ::_thesis: x in BCK-part X
 ex x1 being Element of X st
( x \ y = x1 & 0. X <= x1 ) by A2;
then  (x \ y) ` = 0. X by BCIALG_1:def_11;
then A4: (x `) \ (y `) = 0. X by BCIALG_1:9;
 ex x2 being Element of X st
( y = x2 & 0. X <= x2 ) by A3;
then  (x `) \ (0. X) = 0. X by A4, BCIALG_1:def_11;
then  (0. X) \ x = 0. X by BCIALG_1:2;
then  0. X <= x by BCIALG_1:def_11;
hence  x in BCK-part X ; ::_thesis: verum
end;
A5: for x, y, z being Element of X st (x \ y) \ z in BCK-part X & z in BCK-part X holds
x \ (y \ (y \ x)) in BCK-part X
proof
let x, y, z be Element of X; ::_thesis: ( (x \ y) \ z in BCK-part X & z in BCK-part X implies x \ (y \ (y \ x)) in BCK-part X )
assume that
 (x \ y) \ z in BCK-part X and
 z in BCK-part X ; ::_thesis: x \ (y \ (y \ x)) in BCK-part X
(0. X) \ (x \ (y \ (y \ x))) = (x \ (y \ (y \ x))) `
.= 0. X by BCIALG_1:def_8 ;
then  0. X <= x \ (y \ (y \ x)) by BCIALG_1:def_11;
hence  x \ (y \ (y \ x)) in BCK-part X ; ::_thesis: verum
end;
 0. X in BCK-part X by BCIALG_1:19;
hence  BCK-part X is commutative Ideal of X by A1, A5, Def6, BCIALG_1:def_18; ::_thesis: verum
end;

theorem :: BCIIDEAL:24
for X being BCK-algebra st X is p-Semisimple BCI-algebra holds
{(0. X)} is commutative Ideal of X
proof
let X be BCK-algebra; ::_thesis: ( X is p-Semisimple BCI-algebra implies {(0. X)} is commutative Ideal of X )
set X1 = {(0. X)};
A1: {(0. X)} c= the carrier of X
proof
let xx be set ; :: according to TARSKI:def_3 ::_thesis: ( not xx in {(0. X)} or xx in the carrier of X )
assume  xx in {(0. X)} ; ::_thesis: xx in the carrier of X
then  xx = 0. X by TARSKI:def_1;
hence  xx in the carrier of X ; ::_thesis: verum
end;
A2: for x, y being Element of X st x \ y in {(0. X)} & y in {(0. X)} holds
x in {(0. X)}
proof
set X1 = {(0. X)};
let x, y be Element of X; ::_thesis: ( x \ y in {(0. X)} & y in {(0. X)} implies x in {(0. X)} )
assume  ( x \ y in {(0. X)} & y in {(0. X)} ) ; ::_thesis: x in {(0. X)}
then  ( x \ y = 0. X & y = 0. X ) by TARSKI:def_1;
then  x = 0. X by BCIALG_1:2;
hence  x in {(0. X)} by TARSKI:def_1; ::_thesis: verum
end;
 0. X in {(0. X)} by TARSKI:def_1;
then reconsider X1 = {(0. X)} as Ideal of X by A1, A2, BCIALG_1:def_18;
assume A3: X is p-Semisimple BCI-algebra ; ::_thesis: {(0. X)} is commutative Ideal of X
 for x, y, z being Element of X st (x \ y) \ z in X1 & z in X1 holds
x \ (y \ (y \ x)) in X1
proof
let x, y, z be Element of X; ::_thesis: ( (x \ y) \ z in X1 & z in X1 implies x \ (y \ (y \ x)) in X1 )
assume  ( (x \ y) \ z in X1 & z in X1 ) ; ::_thesis: x \ (y \ (y \ x)) in X1
then  ( (x \ y) \ z = 0. X & z = 0. X ) by TARSKI:def_1;
then A4: x \ y = 0. X by BCIALG_1:2;
 y is atom by A3, BCIALG_1:52;
then  x = y by A4, BCIALG_1:def_14;
then  x \ (y \ (y \ x)) = x \ (x \ (0. X)) by BCIALG_1:def_5;
then  x \ (y \ (y \ x)) = x \ x by BCIALG_1:2;
then  x \ (y \ (y \ x)) = 0. X by BCIALG_1:def_5;
hence  x \ (y \ (y \ x)) in X1 by TARSKI:def_1; ::_thesis: verum
end;
hence  {(0. X)} is commutative Ideal of X by Def6; ::_thesis: verum
end;

Lm1:  for X being BCK-algebra holds the carrier of X c= BCK-part X
proof
let X be BCK-algebra; ::_thesis: the carrier of X c= BCK-part X
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier of X or x in BCK-part X )
assume  x in the carrier of X ; ::_thesis: x in BCK-part X
then consider x1 being Element of X such that
A1: x = x1 ;
 x1 ` = 0. X by BCIALG_1:def_8;
then  0. X <= x1 by BCIALG_1:def_11;
hence  x in BCK-part X by A1; ::_thesis: verum
end;

theorem Th25: :: BCIIDEAL:25
for X being BCK-algebra holds BCK-part X = the carrier of X
proof
let X be BCK-algebra; ::_thesis: BCK-part X = the carrier of X
 the carrier of X c= BCK-part X by Lm1;
hence  BCK-part X = the carrier of X by XBOOLE_0:def_10; ::_thesis: verum
end;

theorem :: BCIIDEAL:26
for X being BCI-algebra st ( for X being BCI-algebra
for x, y being Element of X holds (x \ y) \ y = x \ y ) holds
the carrier of X = BCK-part X
proof
let X be BCI-algebra; ::_thesis: ( ( for X being BCI-algebra
for x, y being Element of X holds (x \ y) \ y = x \ y ) implies the carrier of X = BCK-part X )
assume  for X being BCI-algebra
for x, y being Element of X holds (x \ y) \ y = x \ y ; ::_thesis: the carrier of X = BCK-part X
then  X is BCK-algebra by BCIALG_1:13;
hence  the carrier of X = BCK-part X by Th25; ::_thesis: verum
end;

theorem :: BCIIDEAL:27
for X being BCI-algebra st ( for X being BCI-algebra
for x, y being Element of X holds x \ (y \ x) = x ) holds
the carrier of X = BCK-part X
proof
let X be BCI-algebra; ::_thesis: ( ( for X being BCI-algebra
for x, y being Element of X holds x \ (y \ x) = x ) implies the carrier of X = BCK-part X )
assume  for X being BCI-algebra
for x, y being Element of X holds x \ (y \ x) = x ; ::_thesis: the carrier of X = BCK-part X
then  X is BCK-algebra by BCIALG_1:14;
hence  the carrier of X = BCK-part X by Th25; ::_thesis: verum
end;

theorem :: BCIIDEAL:28
for X being BCI-algebra st ( for X being BCI-algebra
for x, y being Element of X holds x \ (x \ y) = y \ (y \ x) ) holds
the carrier of X = BCK-part X
proof
let X be BCI-algebra; ::_thesis: ( ( for X being BCI-algebra
for x, y being Element of X holds x \ (x \ y) = y \ (y \ x) ) implies the carrier of X = BCK-part X )
assume  for X being BCI-algebra
for x, y being Element of X holds x \ (x \ y) = y \ (y \ x) ; ::_thesis: the carrier of X = BCK-part X
then  X is BCK-algebra by BCIALG_1:12;
hence  the carrier of X = BCK-part X by Th25; ::_thesis: verum
end;

theorem :: BCIIDEAL:29
for X being BCI-algebra st ( for X being BCI-algebra
for x, y, z being Element of X holds (x \ y) \ y = (x \ z) \ (y \ z) ) holds
the carrier of X = BCK-part X
proof
let X be BCI-algebra; ::_thesis: ( ( for X being BCI-algebra
for x, y, z being Element of X holds (x \ y) \ y = (x \ z) \ (y \ z) ) implies the carrier of X = BCK-part X )
assume  for X being BCI-algebra
for x, y, z being Element of X holds (x \ y) \ y = (x \ z) \ (y \ z) ; ::_thesis: the carrier of X = BCK-part X
then  X is BCK-algebra by BCIALG_1:15;
hence  the carrier of X = BCK-part X by Th25; ::_thesis: verum
end;

theorem :: BCIIDEAL:30
for X being BCI-algebra st ( for X being BCI-algebra
for x, y being Element of X holds (x \ y) \ (y \ x) = x \ y ) holds
the carrier of X = BCK-part X
proof
let X be BCI-algebra; ::_thesis: ( ( for X being BCI-algebra
for x, y being Element of X holds (x \ y) \ (y \ x) = x \ y ) implies the carrier of X = BCK-part X )
assume  for X being BCI-algebra
for x, y being Element of X holds (x \ y) \ (y \ x) = x \ y ; ::_thesis: the carrier of X = BCK-part X
then  X is BCK-algebra by BCIALG_1:16;
hence  the carrier of X = BCK-part X by Th25; ::_thesis: verum
end;

theorem :: BCIIDEAL:31
for X being BCI-algebra st ( for X being BCI-algebra
for x, y being Element of X holds (x \ y) \ ((x \ y) \ (y \ x)) = 0. X ) holds
the carrier of X = BCK-part X
proof
let X be BCI-algebra; ::_thesis: ( ( for X being BCI-algebra
for x, y being Element of X holds (x \ y) \ ((x \ y) \ (y \ x)) = 0. X ) implies the carrier of X = BCK-part X )
assume  for X being BCI-algebra
for x, y being Element of X holds (x \ y) \ ((x \ y) \ (y \ x)) = 0. X ; ::_thesis: the carrier of X = BCK-part X
then  X is BCK-algebra by BCIALG_1:17;
hence  the carrier of X = BCK-part X by Th25; ::_thesis: verum
end;

theorem :: BCIIDEAL:32
for X being BCK-algebra holds the carrier of X is commutative Ideal of X
proof
let X be BCK-algebra; ::_thesis: the carrier of X is commutative Ideal of X
set B = BCK-part X;
A1: for x, y being Element of X st x \ y in BCK-part X & y in BCK-part X holds
x in BCK-part X
proof
let x, y be Element of X; ::_thesis: ( x \ y in BCK-part X & y in BCK-part X implies x in BCK-part X )
assume that
A2: x \ y in BCK-part X and
A3: y in BCK-part X ; ::_thesis: x in BCK-part X
 ex x1 being Element of X st
( x \ y = x1 & 0. X <= x1 ) by A2;
then  (x \ y) ` = 0. X by BCIALG_1:def_11;
then A4: (x `) \ (y `) = 0. X by BCIALG_1:9;
 ex x2 being Element of X st
( y = x2 & 0. X <= x2 ) by A3;
then  (x `) \ (0. X) = 0. X by A4, BCIALG_1:def_11;
then  (0. X) \ x = 0. X by BCIALG_1:2;
then  0. X <= x by BCIALG_1:def_11;
hence  x in BCK-part X ; ::_thesis: verum
end;
A5: for x, y, z being Element of X st (x \ y) \ z in BCK-part X & z in BCK-part X holds
x \ (y \ (y \ x)) in BCK-part X
proof
let x, y, z be Element of X; ::_thesis: ( (x \ y) \ z in BCK-part X & z in BCK-part X implies x \ (y \ (y \ x)) in BCK-part X )
assume that
 (x \ y) \ z in BCK-part X and
 z in BCK-part X ; ::_thesis: x \ (y \ (y \ x)) in BCK-part X
(0. X) \ (x \ (y \ (y \ x))) = (x \ (y \ (y \ x))) `
.= 0. X by BCIALG_1:def_8 ;
then  0. X <= x \ (y \ (y \ x)) by BCIALG_1:def_11;
hence  x \ (y \ (y \ x)) in BCK-part X ; ::_thesis: verum
end;
 the carrier of X = BCK-part X by Th25;
hence  the carrier of X is commutative Ideal of X by A1, A5, Def6, BCIALG_1:def_18; ::_thesis: verum
end;


theorem Th33: :: BCIIDEAL:33
for X being BCK-algebra
for I being Ideal of X holds
( I is commutative Ideal of X iff for x, y being Element of X st x \ y in I holds
x \ (y \ (y \ x)) in I )
proof
let X be BCK-algebra; ::_thesis: for I being Ideal of X holds
( I is commutative Ideal of X iff for x, y being Element of X st x \ y in I holds
x \ (y \ (y \ x)) in I )
let I be Ideal of X; ::_thesis: ( I is commutative Ideal of X iff for x, y being Element of X st x \ y in I holds
x \ (y \ (y \ x)) in I )
thus  ( I is commutative Ideal of X implies for x, y being Element of X st x \ y in I holds
x \ (y \ (y \ x)) in I ) ::_thesis: ( ( for x, y being Element of X st x \ y in I holds
x \ (y \ (y \ x)) in I ) implies I is commutative Ideal of X )
proof
A1: 0. X in I by BCIALG_1:def_18;
assume A2: I is commutative Ideal of X ; ::_thesis: for x, y being Element of X st x \ y in I holds
x \ (y \ (y \ x)) in I
let x, y be Element of X; ::_thesis: ( x \ y in I implies x \ (y \ (y \ x)) in I )
assume  x \ y in I ; ::_thesis: x \ (y \ (y \ x)) in I
then  (x \ y) \ (0. X) in I by BCIALG_1:2;
hence  x \ (y \ (y \ x)) in I by A2, A1, Def6; ::_thesis: verum
end;
assume A3: for x, y being Element of X st x \ y in I holds
x \ (y \ (y \ x)) in I ; ::_thesis: I is commutative Ideal of X
 for x, y, z being Element of X st (x \ y) \ z in I & z in I holds
x \ (y \ (y \ x)) in I
proof
let x, y, z be Element of X; ::_thesis: ( (x \ y) \ z in I & z in I implies x \ (y \ (y \ x)) in I )
assume  ( (x \ y) \ z in I & z in I ) ; ::_thesis: x \ (y \ (y \ x)) in I
then  x \ y in I by BCIALG_1:def_18;
hence  x \ (y \ (y \ x)) in I by A3; ::_thesis: verum
end;
hence  I is commutative Ideal of X by Def6; ::_thesis: verum
end;

theorem Th34: :: BCIIDEAL:34
for X being BCK-algebra
for I, A being Ideal of X st I c= A & I is commutative Ideal of X holds
A is commutative Ideal of X
proof
let X be BCK-algebra; ::_thesis: for I, A being Ideal of X st I c= A & I is commutative Ideal of X holds
A is commutative Ideal of X
let I, A be Ideal of X; ::_thesis: ( I c= A & I is commutative Ideal of X implies A is commutative Ideal of X )
assume that
A1: I c= A and
A2: I is commutative Ideal of X ; ::_thesis: A is commutative Ideal of X
 for x, y being Element of X st x \ y in A holds
x \ (y \ (y \ x)) in A
proof
let x, y be Element of X; ::_thesis: ( x \ y in A implies x \ (y \ (y \ x)) in A )
A3: for x, y, z, u being Element of X st x <= y holds
u \ (z \ x) <= u \ (z \ y)
proof
let x, y, z, u be Element of X; ::_thesis: ( x <= y implies u \ (z \ x) <= u \ (z \ y) )
assume  x <= y ; ::_thesis: u \ (z \ x) <= u \ (z \ y)
then  z \ y <= z \ x by BCIALG_1:5;
hence  u \ (z \ x) <= u \ (z \ y) by BCIALG_1:5; ::_thesis: verum
end;
(x \ (x \ y)) \ x = (x \ x) \ (x \ y) by BCIALG_1:7
.= (x \ y) ` by BCIALG_1:def_5
.= 0. X by BCIALG_1:def_8 ;
then  x \ (x \ y) <= x by BCIALG_1:def_11;
then  y \ (y \ (x \ (x \ y))) <= y \ (y \ x) by A3;
then A4: x \ (y \ (y \ x)) <= x \ (y \ (y \ (x \ (x \ y)))) by BCIALG_1:5;
(x \ (x \ y)) \ y = (x \ y) \ (x \ y) by BCIALG_1:7
.= 0. X by BCIALG_1:def_5 ;
then  (x \ (x \ y)) \ y in I by BCIALG_1:def_18;
then  (x \ (x \ y)) \ (y \ (y \ (x \ (x \ y)))) in I by A2, Th33;
then  (x \ (x \ y)) \ (y \ (y \ (x \ (x \ y)))) in A by A1;
then A5: (x \ (y \ (y \ (x \ (x \ y))))) \ (x \ y) in A by BCIALG_1:7;
assume  x \ y in A ; ::_thesis: x \ (y \ (y \ x)) in A
then  x \ (y \ (y \ (x \ (x \ y)))) in A by A5, BCIALG_1:def_18;
hence  x \ (y \ (y \ x)) in A by A4, Th5; ::_thesis: verum
end;
hence  A is commutative Ideal of X by Th33; ::_thesis: verum
end;

theorem Th35: :: BCIIDEAL:35
for X being BCK-algebra holds
( ( for I being Ideal of X holds I is commutative Ideal of X ) iff {(0. X)} is commutative Ideal of X )
proof
let X be BCK-algebra; ::_thesis: ( ( for I being Ideal of X holds I is commutative Ideal of X ) iff {(0. X)} is commutative Ideal of X )
thus  ( ( for I being Ideal of X holds I is commutative Ideal of X ) implies {(0. X)} is commutative Ideal of X ) by BCIALG_1:43; ::_thesis: ( {(0. X)} is commutative Ideal of X implies for I being Ideal of X holds I is commutative Ideal of X )
thus  ( {(0. X)} is commutative Ideal of X implies for I being Ideal of X holds I is commutative Ideal of X ) ::_thesis: verum
proof
assume A1: {(0. X)} is commutative Ideal of X ; ::_thesis: for I being Ideal of X holds I is commutative Ideal of X
let I be Ideal of X; ::_thesis: I is commutative Ideal of X
 for I being Ideal of X holds {(0. X)} c= I
proof
let I be Ideal of X; ::_thesis: {(0. X)} c= I
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {(0. X)} or x in I )
assume  x in {(0. X)} ; ::_thesis: x in I
then  x = 0. X by TARSKI:def_1;
hence  x in I by BCIALG_1:def_18; ::_thesis: verum
end;
hence  I is commutative Ideal of X by A1, Th34; ::_thesis: verum
end;
end;

theorem Th36: :: BCIIDEAL:36
for X being BCK-algebra holds
( {(0. X)} is commutative Ideal of X iff X is commutative BCK-algebra )
proof
let X be BCK-algebra; ::_thesis: ( {(0. X)} is commutative Ideal of X iff X is commutative BCK-algebra )
A1: ( X is commutative BCK-algebra implies for x, y being Element of X holds x \ y = x \ (y \ (y \ x)) )
proof
assume A2: X is commutative BCK-algebra ; ::_thesis: for x, y being Element of X holds x \ y = x \ (y \ (y \ x))
let x, y be Element of X; ::_thesis: x \ y = x \ (y \ (y \ x))
x \ y = x \ (x \ (x \ y)) by BCIALG_1:8
.= x \ (y \ (y \ x)) by A2, BCIALG_3:def_1 ;
hence  x \ y = x \ (y \ (y \ x)) ; ::_thesis: verum
end;
thus  ( {(0. X)} is commutative Ideal of X implies X is commutative BCK-algebra ) ::_thesis: ( X is commutative BCK-algebra implies {(0. X)} is commutative Ideal of X )
proof
assume A3: {(0. X)} is commutative Ideal of X ; ::_thesis: X is commutative BCK-algebra
 for x, y being Element of X st x <= y holds
x = y \ (y \ x)
proof
let x, y be Element of X; ::_thesis: ( x <= y implies x = y \ (y \ x) )
assume  x <= y ; ::_thesis: x = y \ (y \ x)
then  x \ y = 0. X by BCIALG_1:def_11;
then  x \ y in {(0. X)} by TARSKI:def_1;
then  x \ (y \ (y \ x)) in {(0. X)} by A3, Th33;
then  ( (y \ (y \ x)) \ x = 0. X & x \ (y \ (y \ x)) = 0. X ) by BCIALG_1:1, TARSKI:def_1;
hence  x = y \ (y \ x) by BCIALG_1:def_7; ::_thesis: verum
end;
hence  X is commutative BCK-algebra by BCIALG_3:5; ::_thesis: verum
end;
assume  X is commutative BCK-algebra ; ::_thesis: {(0. X)} is commutative Ideal of X
then  for x, y being Element of X st x \ y in {(0. X)} holds
x \ (y \ (y \ x)) in {(0. X)} by A1;
hence  {(0. X)} is commutative Ideal of X by Th33, BCIALG_1:43; ::_thesis: verum
end;

theorem Th37: :: BCIIDEAL:37
for X being BCK-algebra holds
( X is commutative BCK-algebra iff for I being Ideal of X holds I is commutative Ideal of X )
proof
let X be BCK-algebra; ::_thesis: ( X is commutative BCK-algebra iff for I being Ideal of X holds I is commutative Ideal of X )
thus  ( X is commutative BCK-algebra implies for I being Ideal of X holds I is commutative Ideal of X ) ::_thesis: ( ( for I being Ideal of X holds I is commutative Ideal of X ) implies X is commutative BCK-algebra )
proof
assume  X is commutative BCK-algebra ; ::_thesis: for I being Ideal of X holds I is commutative Ideal of X
then  {(0. X)} is commutative Ideal of X by Th36;
hence  for I being Ideal of X holds I is commutative Ideal of X by Th35; ::_thesis: verum
end;
assume  for I being Ideal of X holds I is commutative Ideal of X ; ::_thesis: X is commutative BCK-algebra
then  {(0. X)} is commutative Ideal of X by Th35;
hence  X is commutative BCK-algebra by Th36; ::_thesis: verum
end;

theorem :: BCIIDEAL:38
for X being BCK-algebra holds
( {(0. X)} is commutative Ideal of X iff for I being Ideal of X holds I is commutative Ideal of X )
proof
let X be BCK-algebra; ::_thesis: ( {(0. X)} is commutative Ideal of X iff for I being Ideal of X holds I is commutative Ideal of X )
thus  ( {(0. X)} is commutative Ideal of X implies for I being Ideal of X holds I is commutative Ideal of X ) ::_thesis: ( ( for I being Ideal of X holds I is commutative Ideal of X ) implies {(0. X)} is commutative Ideal of X )
proof
assume  {(0. X)} is commutative Ideal of X ; ::_thesis: for I being Ideal of X holds I is commutative Ideal of X
then  X is commutative BCK-algebra by Th36;
hence  for I being Ideal of X holds I is commutative Ideal of X by Th37; ::_thesis: verum
end;
assume  for I being Ideal of X holds I is commutative Ideal of X ; ::_thesis: {(0. X)} is commutative Ideal of X
then  X is commutative BCK-algebra by Th37;
hence  {(0. X)} is commutative Ideal of X by Th36; ::_thesis: verum
end;

theorem :: BCIIDEAL:39
for X being BCK-algebra
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 )
proof
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) by BCIALG_1:def_11;
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 by BCIALG_1:def_11;
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
end;

theorem :: BCIIDEAL:40
for X being BCK-algebra holds
( {(0. X)} is commutative Ideal of X iff for x, y being Element of X holds x \ (x \ y) <= y \ (y \ x) )
proof
let X be BCK-algebra; ::_thesis: ( {(0. X)} is commutative Ideal of X iff for x, y being Element of X holds x \ (x \ y) <= y \ (y \ x) )
thus  ( {(0. X)} is commutative Ideal of X implies for x, y being Element of X holds x \ (x \ y) <= y \ (y \ x) ) ::_thesis: ( ( for x, y being Element of X holds x \ (x \ y) <= y \ (y \ x) ) implies {(0. X)} is commutative Ideal of X )
proof
assume  {(0. X)} is commutative Ideal of X ; ::_thesis: for x, y being Element of X holds x \ (x \ y) <= y \ (y \ x)
then  X is commutative BCK-algebra by Th36;
hence  for x, y being Element of X holds x \ (x \ y) <= y \ (y \ x) by BCIALG_3:1; ::_thesis: verum
end;
assume  for x, y being Element of X holds x \ (x \ y) <= y \ (y \ x) ; ::_thesis: {(0. X)} is commutative Ideal of X
then  X is commutative BCK-algebra by BCIALG_3:1;
hence  {(0. X)} is commutative Ideal of X by Th36; ::_thesis: verum
end;

theorem :: BCIIDEAL:41
for X being BCK-algebra holds
( {(0. X)} is commutative Ideal of X iff for x, y being Element of X holds x \ y = x \ (y \ (y \ x)) )
proof
let X be BCK-algebra; ::_thesis: ( {(0. X)} is commutative Ideal of X iff for x, y being Element of X holds x \ y = x \ (y \ (y \ x)) )
thus  ( {(0. X)} is commutative Ideal of X implies for x, y being Element of X holds x \ y = x \ (y \ (y \ x)) ) ::_thesis: ( ( for x, y being Element of X holds x \ y = x \ (y \ (y \ x)) ) implies {(0. X)} is commutative Ideal of X )
proof
assume  {(0. X)} is commutative Ideal of X ; ::_thesis: for x, y being Element of X holds x \ y = x \ (y \ (y \ x))
then  X is commutative BCK-algebra by Th36;
hence  for x, y being Element of X holds x \ y = x \ (y \ (y \ x)) by BCIALG_3:3; ::_thesis: verum
end;
assume  for x, y being Element of X holds x \ y = x \ (y \ (y \ x)) ; ::_thesis: {(0. X)} is commutative Ideal of X
then  X is commutative BCK-algebra by BCIALG_3:3;
hence  {(0. X)} is commutative Ideal of X by Th36; ::_thesis: verum
end;

theorem :: BCIIDEAL:42
for X being BCK-algebra holds
( {(0. X)} is commutative Ideal of X iff for x, y being Element of X holds x \ (x \ y) = y \ (y \ (x \ (x \ y))) )
proof
let X be BCK-algebra; ::_thesis: ( {(0. X)} is commutative Ideal of X iff for x, y being Element of X holds x \ (x \ y) = y \ (y \ (x \ (x \ y))) )
thus  ( {(0. X)} is commutative Ideal of X implies for x, y being Element of X holds x \ (x \ y) = y \ (y \ (x \ (x \ y))) ) ::_thesis: ( ( for x, y being Element of X holds x \ (x \ y) = y \ (y \ (x \ (x \ y))) ) implies {(0. X)} is commutative Ideal of X )
proof
assume  {(0. X)} is commutative Ideal of X ; ::_thesis: for x, y being Element of X holds x \ (x \ y) = y \ (y \ (x \ (x \ y)))
then  X is commutative BCK-algebra by Th36;
hence  for x, y being Element of X holds x \ (x \ y) = y \ (y \ (x \ (x \ y))) by BCIALG_3:4; ::_thesis: verum
end;
assume  for x, y being Element of X holds x \ (x \ y) = y \ (y \ (x \ (x \ y))) ; ::_thesis: {(0. X)} is commutative Ideal of X
then  X is commutative BCK-algebra by BCIALG_3:4;
hence  {(0. X)} is commutative Ideal of X by Th36; ::_thesis: verum
end;

theorem :: BCIIDEAL:43
for X being BCK-algebra holds
( {(0. X)} is commutative Ideal of X iff for x, y being Element of X st x <= y holds
x = y \ (y \ x) )
proof
let X be BCK-algebra; ::_thesis: ( {(0. X)} is commutative Ideal of X iff for x, y being Element of X st x <= y holds
x = y \ (y \ x) )
thus  ( {(0. X)} is commutative Ideal of X implies for x, y being Element of X st x <= y holds
x = y \ (y \ x) ) ::_thesis: ( ( for x, y being Element of X st x <= y holds
x = y \ (y \ x) ) implies {(0. X)} is commutative Ideal of X )
proof
assume  {(0. X)} is commutative Ideal of X ; ::_thesis: for x, y being Element of X st x <= y holds
x = y \ (y \ x)
then  X is commutative BCK-algebra by Th36;
hence  for x, y being Element of X st x <= y holds
x = y \ (y \ x) by BCIALG_3:5; ::_thesis: verum
end;
assume  for x, y being Element of X st x <= y holds
x = y \ (y \ x) ; ::_thesis: {(0. X)} is commutative Ideal of X
then  X is commutative BCK-algebra by BCIALG_3:5;
hence  {(0. X)} is commutative Ideal of X by Th36; ::_thesis: verum
end;

theorem :: BCIIDEAL:44
for X being BCK-algebra st {(0. X)} is commutative Ideal of X holds
( ( for x, y being Element of X holds
( x \ y = x iff y \ (y \ x) = 0. X ) ) & ( for x, y being Element of X st x \ y = x holds
y \ x = y ) & ( for x, y, a being Element of X st y <= a holds
(a \ x) \ (a \ y) = y \ x ) & ( for x, y being Element of X holds
( x \ (y \ (y \ x)) = x \ y & (x \ y) \ ((x \ y) \ x) = x \ y ) ) & ( for x, y, a being Element of X st x <= a holds
(a \ y) \ ((a \ y) \ (a \ x)) = (a \ y) \ (x \ y) ) )
proof
let X be BCK-algebra; ::_thesis: ( {(0. X)} is commutative Ideal of X implies ( ( for x, y being Element of X holds
( x \ y = x iff y \ (y \ x) = 0. X ) ) & ( for x, y being Element of X st x \ y = x holds
y \ x = y ) & ( for x, y, a being Element of X st y <= a holds
(a \ x) \ (a \ y) = y \ x ) & ( for x, y being Element of X holds
( x \ (y \ (y \ x)) = x \ y & (x \ y) \ ((x \ y) \ x) = x \ y ) ) & ( for x, y, a being Element of X st x <= a holds
(a \ y) \ ((a \ y) \ (a \ x)) = (a \ y) \ (x \ y) ) ) )
assume  {(0. X)} is commutative Ideal of X ; ::_thesis: ( ( for x, y being Element of X holds
( x \ y = x iff y \ (y \ x) = 0. X ) ) & ( for x, y being Element of X st x \ y = x holds
y \ x = y ) & ( for x, y, a being Element of X st y <= a holds
(a \ x) \ (a \ y) = y \ x ) & ( for x, y being Element of X holds
( x \ (y \ (y \ x)) = x \ y & (x \ y) \ ((x \ y) \ x) = x \ y ) ) & ( for x, y, a being Element of X st x <= a holds
(a \ y) \ ((a \ y) \ (a \ x)) = (a \ y) \ (x \ y) ) )
then A1: X is commutative BCK-algebra by Th36;
hence  for x, y being Element of X holds
( x \ y = x iff y \ (y \ x) = 0. X ) by BCIALG_3:9; ::_thesis: ( ( for x, y being Element of X st x \ y = x holds
y \ x = y ) & ( for x, y, a being Element of X st y <= a holds
(a \ x) \ (a \ y) = y \ x ) & ( for x, y being Element of X holds
( x \ (y \ (y \ x)) = x \ y & (x \ y) \ ((x \ y) \ x) = x \ y ) ) & ( for x, y, a being Element of X st x <= a holds
(a \ y) \ ((a \ y) \ (a \ x)) = (a \ y) \ (x \ y) ) )
thus  for x, y being Element of X st x \ y = x holds
y \ x = y by A1, BCIALG_3:7; ::_thesis: ( ( for x, y, a being Element of X st y <= a holds
(a \ x) \ (a \ y) = y \ x ) & ( for x, y being Element of X holds
( x \ (y \ (y \ x)) = x \ y & (x \ y) \ ((x \ y) \ x) = x \ y ) ) & ( for x, y, a being Element of X st x <= a holds
(a \ y) \ ((a \ y) \ (a \ x)) = (a \ y) \ (x \ y) ) )
thus  for x, y, a being Element of X st y <= a holds
(a \ x) \ (a \ y) = y \ x by A1, BCIALG_3:8; ::_thesis: ( ( for x, y being Element of X holds
( x \ (y \ (y \ x)) = x \ y & (x \ y) \ ((x \ y) \ x) = x \ y ) ) & ( for x, y, a being Element of X st x <= a holds
(a \ y) \ ((a \ y) \ (a \ x)) = (a \ y) \ (x \ y) ) )
thus  for x, y being Element of X holds
( x \ (y \ (y \ x)) = x \ y & (x \ y) \ ((x \ y) \ x) = x \ y ) by A1, BCIALG_3:10; ::_thesis: for x, y, a being Element of X st x <= a holds
(a \ y) \ ((a \ y) \ (a \ x)) = (a \ y) \ (x \ y)
thus  for x, y, a being Element of X st x <= a holds
(a \ y) \ ((a \ y) \ (a \ x)) = (a \ y) \ (x \ y) by A1, BCIALG_3:11; ::_thesis: verum
end;

theorem :: BCIIDEAL:45
for X being BCK-algebra holds
( ( for I being Ideal of X holds I is commutative Ideal of X ) iff for x, y being Element of X holds x \ (x \ y) <= y \ (y \ x) )
proof
let X be BCK-algebra; ::_thesis: ( ( for I being Ideal of X holds I is commutative Ideal of X ) iff for x, y being Element of X holds x \ (x \ y) <= y \ (y \ x) )
thus  ( ( for I being Ideal of X holds I is commutative Ideal of X ) implies for x, y being Element of X holds x \ (x \ y) <= y \ (y \ x) ) ::_thesis: ( ( for x, y being Element of X holds x \ (x \ y) <= y \ (y \ x) ) implies for I being Ideal of X holds I is commutative Ideal of X )
proof
assume  for I being Ideal of X holds I is commutative Ideal of X ; ::_thesis: for x, y being Element of X holds x \ (x \ y) <= y \ (y \ x)
then  X is commutative BCK-algebra by Th37;
hence  for x, y being Element of X holds x \ (x \ y) <= y \ (y \ x) by BCIALG_3:1; ::_thesis: verum
end;
assume  for x, y being Element of X holds x \ (x \ y) <= y \ (y \ x) ; ::_thesis: for I being Ideal of X holds I is commutative Ideal of X
then  X is commutative BCK-algebra by BCIALG_3:1;
hence  for I being Ideal of X holds I is commutative Ideal of X by Th37; ::_thesis: verum
end;

theorem :: BCIIDEAL:46
for X being BCK-algebra holds
( ( for I being Ideal of X holds I is commutative Ideal of X ) iff for x, y being Element of X holds x \ y = x \ (y \ (y \ x)) )
proof
let X be BCK-algebra; ::_thesis: ( ( for I being Ideal of X holds I is commutative Ideal of X ) iff for x, y being Element of X holds x \ y = x \ (y \ (y \ x)) )
thus  ( ( for I being Ideal of X holds I is commutative Ideal of X ) implies for x, y being Element of X holds x \ y = x \ (y \ (y \ x)) ) ::_thesis: ( ( for x, y being Element of X holds x \ y = x \ (y \ (y \ x)) ) implies for I being Ideal of X holds I is commutative Ideal of X )
proof
assume  for I being Ideal of X holds I is commutative Ideal of X ; ::_thesis: for x, y being Element of X holds x \ y = x \ (y \ (y \ x))
then  X is commutative BCK-algebra by Th37;
hence  for x, y being Element of X holds x \ y = x \ (y \ (y \ x)) by BCIALG_3:3; ::_thesis: verum
end;
assume  for x, y being Element of X holds x \ y = x \ (y \ (y \ x)) ; ::_thesis: for I being Ideal of X holds I is commutative Ideal of X
then  X is commutative BCK-algebra by BCIALG_3:3;
hence  for I being Ideal of X holds I is commutative Ideal of X by Th37; ::_thesis: verum
end;

theorem :: BCIIDEAL:47
for X being BCK-algebra holds
( ( for I being Ideal of X holds I is commutative Ideal of X ) iff for x, y being Element of X holds x \ (x \ y) = y \ (y \ (x \ (x \ y))) )
proof
let X be BCK-algebra; ::_thesis: ( ( for I being Ideal of X holds I is commutative Ideal of X ) iff for x, y being Element of X holds x \ (x \ y) = y \ (y \ (x \ (x \ y))) )
thus  ( ( for I being Ideal of X holds I is commutative Ideal of X ) implies for x, y being Element of X holds x \ (x \ y) = y \ (y \ (x \ (x \ y))) ) ::_thesis: ( ( for x, y being Element of X holds x \ (x \ y) = y \ (y \ (x \ (x \ y))) ) implies for I being Ideal of X holds I is commutative Ideal of X )
proof
assume  for I being Ideal of X holds I is commutative Ideal of X ; ::_thesis: for x, y being Element of X holds x \ (x \ y) = y \ (y \ (x \ (x \ y)))
then  X is commutative BCK-algebra by Th37;
hence  for x, y being Element of X holds x \ (x \ y) = y \ (y \ (x \ (x \ y))) by BCIALG_3:4; ::_thesis: verum
end;
assume  for x, y being Element of X holds x \ (x \ y) = y \ (y \ (x \ (x \ y))) ; ::_thesis: for I being Ideal of X holds I is commutative Ideal of X
then  X is commutative BCK-algebra by BCIALG_3:4;
hence  for I being Ideal of X holds I is commutative Ideal of X by Th37; ::_thesis: verum
end;

theorem :: BCIIDEAL:48
for X being BCK-algebra holds
( ( for I being Ideal of X holds I is commutative Ideal of X ) iff for x, y being Element of X st x <= y holds
x = y \ (y \ x) )
proof
let X be BCK-algebra; ::_thesis: ( ( for I being Ideal of X holds I is commutative Ideal of X ) iff for x, y being Element of X st x <= y holds
x = y \ (y \ x) )
thus  ( ( for I being Ideal of X holds I is commutative Ideal of X ) implies for x, y being Element of X st x <= y holds
x = y \ (y \ x) ) ::_thesis: ( ( for x, y being Element of X st x <= y holds
x = y \ (y \ x) ) implies for I being Ideal of X holds I is commutative Ideal of X )
proof
assume  for I being Ideal of X holds I is commutative Ideal of X ; ::_thesis: for x, y being Element of X st x <= y holds
x = y \ (y \ x)
then  X is commutative BCK-algebra by Th37;
hence  for x, y being Element of X st x <= y holds
x = y \ (y \ x) by BCIALG_3:5; ::_thesis: verum
end;
assume  for x, y being Element of X st x <= y holds
x = y \ (y \ x) ; ::_thesis: for I being Ideal of X holds I is commutative Ideal of X
then  X is commutative BCK-algebra by BCIALG_3:5;
hence  for I being Ideal of X holds I is commutative Ideal of X by Th37; ::_thesis: verum
end;

theorem :: BCIIDEAL:49
for X being BCK-algebra st ( for I being Ideal of X holds I is commutative Ideal of X ) holds
( ( for x, y being Element of X holds
( x \ y = x iff y \ (y \ x) = 0. X ) ) & ( for x, y being Element of X st x \ y = x holds
y \ x = y ) & ( for x, y, a being Element of X st y <= a holds
(a \ x) \ (a \ y) = y \ x ) & ( for x, y being Element of X holds
( x \ (y \ (y \ x)) = x \ y & (x \ y) \ ((x \ y) \ x) = x \ y ) ) & ( for x, y, a being Element of X st x <= a holds
(a \ y) \ ((a \ y) \ (a \ x)) = (a \ y) \ (x \ y) ) )
proof
let X be BCK-algebra; ::_thesis: ( ( for I being Ideal of X holds I is commutative Ideal of X ) implies ( ( for x, y being Element of X holds
( x \ y = x iff y \ (y \ x) = 0. X ) ) & ( for x, y being Element of X st x \ y = x holds
y \ x = y ) & ( for x, y, a being Element of X st y <= a holds
(a \ x) \ (a \ y) = y \ x ) & ( for x, y being Element of X holds
( x \ (y \ (y \ x)) = x \ y & (x \ y) \ ((x \ y) \ x) = x \ y ) ) & ( for x, y, a being Element of X st x <= a holds
(a \ y) \ ((a \ y) \ (a \ x)) = (a \ y) \ (x \ y) ) ) )
assume  for I being Ideal of X holds I is commutative Ideal of X ; ::_thesis: ( ( for x, y being Element of X holds
( x \ y = x iff y \ (y \ x) = 0. X ) ) & ( for x, y being Element of X st x \ y = x holds
y \ x = y ) & ( for x, y, a being Element of X st y <= a holds
(a \ x) \ (a \ y) = y \ x ) & ( for x, y being Element of X holds
( x \ (y \ (y \ x)) = x \ y & (x \ y) \ ((x \ y) \ x) = x \ y ) ) & ( for x, y, a being Element of X st x <= a holds
(a \ y) \ ((a \ y) \ (a \ x)) = (a \ y) \ (x \ y) ) )
then A1: X is commutative BCK-algebra by Th37;
hence  for x, y being Element of X holds
( x \ y = x iff y \ (y \ x) = 0. X ) by BCIALG_3:9; ::_thesis: ( ( for x, y being Element of X st x \ y = x holds
y \ x = y ) & ( for x, y, a being Element of X st y <= a holds
(a \ x) \ (a \ y) = y \ x ) & ( for x, y being Element of X holds
( x \ (y \ (y \ x)) = x \ y & (x \ y) \ ((x \ y) \ x) = x \ y ) ) & ( for x, y, a being Element of X st x <= a holds
(a \ y) \ ((a \ y) \ (a \ x)) = (a \ y) \ (x \ y) ) )
thus  for x, y being Element of X st x \ y = x holds
y \ x = y by A1, BCIALG_3:7; ::_thesis: ( ( for x, y, a being Element of X st y <= a holds
(a \ x) \ (a \ y) = y \ x ) & ( for x, y being Element of X holds
( x \ (y \ (y \ x)) = x \ y & (x \ y) \ ((x \ y) \ x) = x \ y ) ) & ( for x, y, a being Element of X st x <= a holds
(a \ y) \ ((a \ y) \ (a \ x)) = (a \ y) \ (x \ y) ) )
thus  for x, y, a being Element of X st y <= a holds
(a \ x) \ (a \ y) = y \ x by A1, BCIALG_3:8; ::_thesis: ( ( for x, y being Element of X holds
( x \ (y \ (y \ x)) = x \ y & (x \ y) \ ((x \ y) \ x) = x \ y ) ) & ( for x, y, a being Element of X st x <= a holds
(a \ y) \ ((a \ y) \ (a \ x)) = (a \ y) \ (x \ y) ) )
thus  for x, y being Element of X holds
( x \ (y \ (y \ x)) = x \ y & (x \ y) \ ((x \ y) \ x) = x \ y ) by A1, BCIALG_3:10; ::_thesis: for x, y, a being Element of X st x <= a holds
(a \ y) \ ((a \ y) \ (a \ x)) = (a \ y) \ (x \ y)
thus  for x, y, a being Element of X st x <= a holds
(a \ y) \ ((a \ y) \ (a \ x)) = (a \ y) \ (x \ y) by A1, BCIALG_3:11; ::_thesis: verum
end;

begin

definition
let X be BCK-algebra;
mode implicative-ideal of X ->  non empty Subset of X means :Def7: :: BCIIDEAL:def 7
( 0. X in it & ( for x, y, z being Element of X st (x \ (y \ x)) \ z in it & z in it holds
x in it ) );
existence
 ex b1 being non empty Subset of X st
( 0. X in b1 & ( for x, y, z being Element of X st (x \ (y \ x)) \ z in b1 & z in b1 holds
x in b1 ) )
proof
take X1 = the carrier of X; ::_thesis: ( X1 is non empty Subset of X & 0. X in X1 & ( for x, y, z being Element of X st (x \ (y \ x)) \ z in X1 & z in X1 holds
x in X1 ) )
 X1 c= the carrier of X ;
hence  ( X1 is non empty Subset of X & 0. X in X1 & ( for x, y, z being Element of X st (x \ (y \ x)) \ z in X1 & z in X1 holds
x in X1 ) ) ; ::_thesis: verum
end;
end;

:: deftheorem Def7 defines implicative-ideal BCIIDEAL:def_7_:_
 for X being BCK-algebra
for b2 being non empty Subset of X holds
( b2 is implicative-ideal of X iff ( 0. X in b2 & ( for x, y, z being Element of X st (x \ (y \ x)) \ z in b2 & z in b2 holds
x in b2 ) ) );


theorem Th50: :: BCIIDEAL:50
for X being BCK-algebra
for I being Ideal of X holds
( I is implicative-ideal of X iff for x, y being Element of X st x \ (y \ x) in I holds
x in I )
proof
let X be BCK-algebra; ::_thesis: for I being Ideal of X holds
( I is implicative-ideal of X iff for x, y being Element of X st x \ (y \ x) in I holds
x in I )
let I be Ideal of X; ::_thesis: ( I is implicative-ideal of X iff for x, y being Element of X st x \ (y \ x) in I holds
x in I )
A1: ( ( for x, y being Element of X st x \ (y \ x) in I holds
x in I ) implies I is implicative-ideal of X )
proof
assume A2: for x, y being Element of X st x \ (y \ x) in I holds
x in I ; ::_thesis: I is implicative-ideal of X
A3: for x, y, z being Element of X st (x \ (y \ x)) \ z in I & z in I holds
x in I
proof
let x, y, z be Element of X; ::_thesis: ( (x \ (y \ x)) \ z in I & z in I implies x in I )
assume  ( (x \ (y \ x)) \ z in I & z in I ) ; ::_thesis: x in I
then  x \ (y \ x) in I by BCIALG_1:def_18;
hence  x in I by A2; ::_thesis: verum
end;
 0. X in I by BCIALG_1:def_18;
hence  I is implicative-ideal of X by A3, Def7; ::_thesis: verum
end;
 ( I is implicative-ideal of X implies for x, y being Element of X st x \ (y \ x) in I holds
x in I )
proof
assume A4: I is implicative-ideal of X ; ::_thesis: for x, y being Element of X st x \ (y \ x) in I holds
x in I
let x, y be Element of X; ::_thesis: ( x \ (y \ x) in I implies x in I )
assume  x \ (y \ x) in I ; ::_thesis: x in I
then A5: (x \ (y \ x)) \ (0. X) in I by BCIALG_1:2;
thus  x in I by A4, A5, Def7; ::_thesis: verum
end;
hence  ( I is implicative-ideal of X iff for x, y being Element of X st x \ (y \ x) in I holds
x in I ) by A1; ::_thesis: verum
end;

definition
let X be BCK-algebra;
mode positive-implicative-ideal of X ->  non empty Subset of X means :Def8: :: BCIIDEAL:def 8
( 0. X in it & ( for x, y, z being Element of X st (x \ y) \ z in it & y \ z in it holds
x \ z in it ) );
existence
 ex b1 being non empty Subset of X st
( 0. X in b1 & ( for x, y, z being Element of X st (x \ y) \ z in b1 & y \ z in b1 holds
x \ z in b1 ) )
proof
take X1 = the carrier of X; ::_thesis: ( X1 is non empty Subset of X & 0. X in X1 & ( for x, y, z being Element of X st (x \ y) \ z in X1 & y \ z in X1 holds
x \ z in X1 ) )
 X1 c= the carrier of X ;
hence  ( X1 is non empty Subset of X & 0. X in X1 & ( for x, y, z being Element of X st (x \ y) \ z in X1 & y \ z in X1 holds
x \ z in X1 ) ) ; ::_thesis: verum
end;
end;

:: deftheorem Def8 defines positive-implicative-ideal BCIIDEAL:def_8_:_
 for X being BCK-algebra
for b2 being non empty Subset of X holds
( b2 is positive-implicative-ideal of X iff ( 0. X in b2 & ( for x, y, z being Element of X st (x \ y) \ z in b2 & y \ z in b2 holds
x \ z in b2 ) ) );

theorem Th51: :: BCIIDEAL:51
for X being BCK-algebra
for I being Ideal of X holds
( I is positive-implicative-ideal of X iff for x, y being Element of X st (x \ y) \ y in I holds
x \ y in I )
proof
let X be BCK-algebra; ::_thesis: for I being Ideal of X holds
( I is positive-implicative-ideal of X iff for x, y being Element of X st (x \ y) \ y in I holds
x \ y in I )
let I be Ideal of X; ::_thesis: ( I is positive-implicative-ideal of X iff for x, y being Element of X st (x \ y) \ y in I holds
x \ y in I )
thus  ( I is positive-implicative-ideal of X implies for x, y being Element of X st (x \ y) \ y in I holds
x \ y in I ) ::_thesis: ( ( for x, y being Element of X st (x \ y) \ y in I holds
x \ y in I ) implies I is positive-implicative-ideal of X )
proof
assume A1: I is positive-implicative-ideal of X ; ::_thesis: for x, y being Element of X st (x \ y) \ y in I holds
x \ y in I
let x, y be Element of X; ::_thesis: ( (x \ y) \ y in I implies x \ y in I )
 y \ y = 0. X by BCIALG_1:def_5;
then A2: y \ y in I by A1, Def8;
assume  (x \ y) \ y in I ; ::_thesis: x \ y in I
hence  x \ y in I by A1, A2, Def8; ::_thesis: verum
end;
thus  ( ( for x, y being Element of X st (x \ y) \ y in I holds
x \ y in I ) implies I is positive-implicative-ideal of X ) ::_thesis: verum
proof
assume A3: for x, y being Element of X st (x \ y) \ y in I holds
x \ y in I ; ::_thesis: I is positive-implicative-ideal of X
A4: for x, y, z being Element of X st (x \ y) \ z in I & y \ z in I holds
x \ z in I
proof
let x, y, z be Element of X; ::_thesis: ( (x \ y) \ z in I & y \ z in I implies x \ z in I )
assume that
A5: (x \ y) \ z in I and
A6: y \ z in I ; ::_thesis: x \ z in I
 (((x \ z) \ z) \ ((x \ y) \ z)) \ ((x \ z) \ (x \ y)) = 0. X by BCIALG_1:def_3;
then  ((x \ z) \ z) \ ((x \ y) \ z) <= (x \ z) \ (x \ y) by BCIALG_1:def_11;
then  (((x \ z) \ z) \ ((x \ y) \ z)) \ (y \ z) <= ((x \ z) \ (x \ y)) \ (y \ z) by BCIALG_1:5;
then  (((x \ z) \ z) \ ((x \ y) \ z)) \ (y \ z) <= 0. X by BCIALG_1:1;
then  ((((x \ z) \ z) \ ((x \ y) \ z)) \ (y \ z)) \ (0. X) = 0. X by BCIALG_1:def_11;
then  (((x \ z) \ z) \ ((x \ y) \ z)) \ (y \ z) = 0. X by BCIALG_1:2;
then  ((x \ z) \ z) \ ((x \ y) \ z) <= y \ z by BCIALG_1:def_11;
then  ((x \ z) \ z) \ ((x \ y) \ z) in I by A6, Th5;
then  (x \ z) \ z in I by A5, BCIALG_1:def_18;
hence  x \ z in I by A3; ::_thesis: verum
end;
 0. X in I by BCIALG_1:def_18;
hence  I is positive-implicative-ideal of X by A4, Def8; ::_thesis: verum
end;
end;

theorem Th52: :: BCIIDEAL:52
for X being BCK-algebra
for I being Ideal of X st ( for x, y, z being Element of X st (x \ y) \ z in I & y \ z in I holds
x \ z in I ) holds
for x, y, z being Element of X st (x \ y) \ z in I holds
(x \ z) \ (y \ z) in I
proof
let X be BCK-algebra; ::_thesis: for I being Ideal of X st ( for x, y, z being Element of X st (x \ y) \ z in I & y \ z in I holds
x \ z in I ) holds
for x, y, z being Element of X st (x \ y) \ z in I holds
(x \ z) \ (y \ z) in I
let I be Ideal of X; ::_thesis: ( ( for x, y, z being Element of X st (x \ y) \ z in I & y \ z in I holds
x \ z in I ) implies for x, y, z being Element of X st (x \ y) \ z in I holds
(x \ z) \ (y \ z) in I )
assume A1: for x, y, z being Element of X st (x \ y) \ z in I & y \ z in I holds
x \ z in I ; ::_thesis: for x, y, z being Element of X st (x \ y) \ z in I holds
(x \ z) \ (y \ z) in I
let x, y, z be Element of X; ::_thesis: ( (x \ y) \ z in I implies (x \ z) \ (y \ z) in I )
 ((x \ (y \ z)) \ (x \ y)) \ (y \ (y \ z)) = 0. X by BCIALG_1:1;
then  (x \ (y \ z)) \ (x \ y) <= y \ (y \ z) by BCIALG_1:def_11;
then A2: ((x \ (y \ z)) \ (x \ y)) \ z <= (y \ (y \ z)) \ z by BCIALG_1:5;
 (y \ (y \ z)) \ z = (y \ z) \ (y \ z) by BCIALG_1:7;
then  ((x \ (y \ z)) \ (x \ y)) \ z <= 0. X by A2, BCIALG_1:def_5;
then  (((x \ (y \ z)) \ (x \ y)) \ z) \ (0. X) = 0. X by BCIALG_1:def_11;
then  ((x \ (y \ z)) \ (x \ y)) \ z = 0. X by BCIALG_1:2;
then A3: ((x \ (y \ z)) \ (x \ y)) \ z in I by BCIALG_1:def_18;
assume  (x \ y) \ z in I ; ::_thesis: (x \ z) \ (y \ z) in I
then  (x \ (y \ z)) \ z in I by A1, A3;
hence  (x \ z) \ (y \ z) in I by BCIALG_1:7; ::_thesis: verum
end;

theorem Th53: :: BCIIDEAL:53
for X being BCK-algebra
for I being Ideal of X st ( for x, y, z being Element of X st (x \ y) \ z in I holds
(x \ z) \ (y \ z) in I ) holds
I is positive-implicative-ideal of X
proof
let X be BCK-algebra; ::_thesis: for I being Ideal of X st ( for x, y, z being Element of X st (x \ y) \ z in I holds
(x \ z) \ (y \ z) in I ) holds
I is positive-implicative-ideal of X
let I be Ideal of X; ::_thesis: ( ( for x, y, z being Element of X st (x \ y) \ z in I holds
(x \ z) \ (y \ z) in I ) implies I is positive-implicative-ideal of X )
assume A1: for x, y, z being Element of X st (x \ y) \ z in I holds
(x \ z) \ (y \ z) in I ; ::_thesis: I is positive-implicative-ideal of X
A2: for x, y, z being Element of X st (x \ y) \ z in I & y \ z in I holds
x \ z in I
proof
let x, y, z be Element of X; ::_thesis: ( (x \ y) \ z in I & y \ z in I implies x \ z in I )
assume that
A3: (x \ y) \ z in I and
A4: y \ z in I ; ::_thesis: x \ z in I
 (x \ z) \ (y \ z) in I by A1, A3;
hence  x \ z in I by A4, BCIALG_1:def_18; ::_thesis: verum
end;
 0. X in I by BCIALG_1:def_18;
hence  I is positive-implicative-ideal of X by A2, Def8; ::_thesis: verum
end;

theorem :: BCIIDEAL:54
for X being BCK-algebra
for I being Ideal of X holds
( I is positive-implicative-ideal of X iff for x, y, z being Element of X st (x \ y) \ z in I & y \ z in I holds
x \ z in I )
proof
let X be BCK-algebra; ::_thesis: for I being Ideal of X holds
( I is positive-implicative-ideal of X iff for x, y, z being Element of X st (x \ y) \ z in I & y \ z in I holds
x \ z in I )
let I be Ideal of X; ::_thesis: ( I is positive-implicative-ideal of X iff for x, y, z being Element of X st (x \ y) \ z in I & y \ z in I holds
x \ z in I )
A1: 0. X in I by BCIALG_1:def_18;
thus  ( I is positive-implicative-ideal of X implies for x, y, z being Element of X st (x \ y) \ z in I & y \ z in I holds
x \ z in I ) by Def8; ::_thesis: ( ( for x, y, z being Element of X st (x \ y) \ z in I & y \ z in I holds
x \ z in I ) implies I is positive-implicative-ideal of X )
assume  for x, y, z being Element of X st (x \ y) \ z in I & y \ z in I holds
x \ z in I ; ::_thesis: I is positive-implicative-ideal of X
hence  I is positive-implicative-ideal of X by A1, Def8; ::_thesis: verum
end;

theorem :: BCIIDEAL:55
for X being BCK-algebra
for I being Ideal of X holds
( I is positive-implicative-ideal of X iff for x, y, z being Element of X st (x \ y) \ z in I holds
(x \ z) \ (y \ z) in I )
proof
let X be BCK-algebra; ::_thesis: for I being Ideal of X holds
( I is positive-implicative-ideal of X iff for x, y, z being Element of X st (x \ y) \ z in I holds
(x \ z) \ (y \ z) in I )
let I be Ideal of X; ::_thesis: ( I is positive-implicative-ideal of X iff for x, y, z being Element of X st (x \ y) \ z in I holds
(x \ z) \ (y \ z) in I )
 ( I is positive-implicative-ideal of X implies for x, y, z being Element of X st (x \ y) \ z in I & y \ z in I holds
x \ z in I ) by Def8;
hence  ( I is positive-implicative-ideal of X iff for x, y, z being Element of X st (x \ y) \ z in I holds
(x \ z) \ (y \ z) in I ) by Th52, Th53; ::_thesis: verum
end;

theorem :: BCIIDEAL:56
for X being BCK-algebra
for I, A being Ideal of X st I c= A & I is positive-implicative-ideal of X holds
A is positive-implicative-ideal of X
proof
let X be BCK-algebra; ::_thesis: for I, A being Ideal of X st I c= A & I is positive-implicative-ideal of X holds
A is positive-implicative-ideal of X
let I, A be Ideal of X; ::_thesis: ( I c= A & I is positive-implicative-ideal of X implies A is positive-implicative-ideal of X )
assume that
A1: I c= A and
A2: I is positive-implicative-ideal of X ; ::_thesis: A is positive-implicative-ideal of X
 for x, y being Element of X st (x \ y) \ y in A holds
x \ y in A
proof
let x, y be Element of X; ::_thesis: ( (x \ y) \ y in A implies x \ y in A )
((x \ ((x \ y) \ y)) \ y) \ y = ((x \ y) \ ((x \ y) \ y)) \ y by BCIALG_1:7
.= ((x \ y) \ y) \ ((x \ y) \ y) by BCIALG_1:7
.= 0. X by BCIALG_1:def_5 ;
then  ((x \ ((x \ y) \ y)) \ y) \ y in I by BCIALG_1:def_18;
then  (x \ ((x \ y) \ y)) \ y in I by A2, Th51;
then A3: (x \ y) \ ((x \ y) \ y) in I by BCIALG_1:7;
assume  (x \ y) \ y in A ; ::_thesis: x \ y in A
hence  x \ y in A by A1, A3, BCIALG_1:def_18; ::_thesis: verum
end;
hence  A is positive-implicative-ideal of X by Th51; ::_thesis: verum
end;

theorem :: BCIIDEAL:57
for X being BCK-algebra
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 )
proof
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
proof
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 by BCIALG_1:def_11;
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 by BCIALG_1:def_11;
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 by BCIALG_1:def_11;
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;
 for x, y being Element of X st (x \ y) \ y in I holds
x \ y in I
proof
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 by BCIALG_1:def_11;
assume  (x \ y) \ y in I ; ::_thesis: x \ y in I
hence  x \ y in I by A1, A5, Th5, Th50; ::_thesis: verum
end;
hence  ( I is commutative Ideal of X & I is positive-implicative-ideal of X ) by A2, Th33, Th51; ::_thesis: verum
end;