:: by Chenglong Wu and Yuzhong Ding

::

:: Received March 3, 2008

:: Copyright (c) 2008-2021 Association of Mizar Users

::P20

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)

for x, y, z, u being Element of X st x <= y holds

u \ (z \ x) <= u \ (z \ y)

proof 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

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

proof 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

for x, y, z, u, v being Element of X holds (x \ (y \ (z \ u))) \ (x \ (y \ (z \ v))) <= v \ u

proof end;

::P26

definition

let X be BCI-algebra;

let a be Element of X;

coherence

{ x where x is Element of X : x <= a } is set ;

end;
let a be Element of X;

coherence

{ x where x is Element of X : x <= a } is set ;

:: 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 } ;

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

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 end;

::P37

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

for x, a, b being Element of AtomSet X st x is Element of BranchV b holds

a \ x = a \ b

proof 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

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 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

for A being Ideal of X

for a being Element of A holds initial_section a c= A

proof 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

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 end;

::p47

:: 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 );

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 );

::P48

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 )

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 end;

::P50

theorem :: BCIIDEAL:13

for X being BCI-algebra

for A being Ideal of X st X is quasi-associative holds

A is closed by BCIALG_1:71, Th5;

for A being Ideal of X st X is quasi-associative holds

A is closed by BCIALG_1:71, Th5;

:: 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 ) ) );

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
end;

definition

let X be BCI-algebra;

ex b_{1} being non empty Subset of X st

( 0. X in b_{1} & ( for x, y, z being Element of X st (x \ y) \ z in b_{1} & y \ z in b_{1} holds

x in b_{1} ) )

end;
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 ( 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 ) );

ex b

( 0. X in b

x in b

proof end;

:: deftheorem Def4 defines associative-ideal BCIIDEAL:def 4 :

for X being BCI-algebra

for b_{2} being non empty Subset of X holds

( b_{2} is associative-ideal of X iff ( 0. X in b_{2} & ( for x, y, z being Element of X st (x \ y) \ z in b_{2} & y \ z in b_{2} holds

x in b_{2} ) ) );

for X being BCI-algebra

for b

( b

x in b

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

for X1 being non empty Subset of X st X1 is associative-ideal of X holds

X1 is Ideal of X

proof 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 )

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 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

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 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

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 end;

definition

let X be BCI-algebra;

ex b_{1} being non empty Subset of X st

( 0. X in b_{1} & ( for x, y, z being Element of X st (x \ z) \ (y \ z) in b_{1} & y in b_{1} holds

x in b_{1} ) )

end;
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 ( 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 ) );

ex b

( 0. X in b

x in b

proof end;

:: deftheorem Def5 defines p-ideal BCIIDEAL:def 5 :

for X being BCI-algebra

for b_{2} being non empty Subset of X holds

( b_{2} is p-ideal of X iff ( 0. X in b_{2} & ( for x, y, z being Element of X st (x \ z) \ (y \ z) in b_{2} & y in b_{2} holds

x in b_{2} ) ) );

for X being BCI-algebra

for b

( b

x in b

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

for X1 being non empty Subset of X st X1 is p-ideal of X holds

X1 is Ideal of X

proof 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 )

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 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 )

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 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 );

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
end;

Lm1: for X being BCK-algebra holds the carrier of X c= BCK-part X

proof 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

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

the carrier of X = BCK-part X

proof 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

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

the carrier of X = BCK-part X

proof 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

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

the carrier of X = BCK-part X

proof 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

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 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

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

the carrier of X = BCK-part X

proof 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

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 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 )

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 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

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 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 )

( ( for I being Ideal of X holds I is commutative Ideal of X ) iff {(0. X)} is commutative Ideal of X )

proof end;

theorem Th36: :: BCIIDEAL:36

for X being BCK-algebra holds

( {(0. X)} is commutative Ideal of X iff X is commutative BCK-algebra )

( {(0. X)} is commutative Ideal of X iff X is commutative BCK-algebra )

proof 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 )

( X is commutative BCK-algebra iff for I being Ideal of X holds I is commutative Ideal of X )

proof 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 ) by Th37, Th36;

( {(0. X)} is commutative Ideal of X iff for I being Ideal of X holds I is commutative Ideal of X ) by Th37, Th36;

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 )

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 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) ) by BCIALG_3:1, Th36;

( {(0. X)} is commutative Ideal of X iff for x, y being Element of X holds x \ (x \ y) <= y \ (y \ x) ) by BCIALG_3:1, Th36;

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)) ) by BCIALG_3:3, Th36;

( {(0. X)} is commutative Ideal of X iff for x, y being Element of X holds x \ y = x \ (y \ (y \ x)) ) by BCIALG_3:3, Th36;

theorem :: BCIIDEAL:42

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) ) by BCIALG_3:5, Th36;

( {(0. X)} is commutative Ideal of X iff for x, y being Element of X st x <= y holds

x = y \ (y \ x) ) by BCIALG_3:5, Th36;

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) ) )

( ( 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 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) ) by BCIALG_3:1, Th37;

( ( 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) ) by BCIALG_3:1, Th37;

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)) ) by BCIALG_3:3, Th37;

( ( 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)) ) by BCIALG_3:3, Th37;

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))) ) by BCIALG_3:4, Th37;

( ( 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))) ) by BCIALG_3:4, Th37;

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) ) by BCIALG_3:5, Th37;

( ( 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) ) by BCIALG_3:5, Th37;

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) ) )

( ( 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 end;

definition

let X be BCK-algebra;

ex b_{1} being non empty Subset of X st

( 0. X in b_{1} & ( for x, y, z being Element of X st (x \ (y \ x)) \ z in b_{1} & z in b_{1} holds

x in b_{1} ) )

end;
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 ( 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 ) );

ex b

( 0. X in b

x in b

proof end;

:: deftheorem Def7 defines implicative-ideal BCIIDEAL:def 7 :

for X being BCK-algebra

for b_{2} being non empty Subset of X holds

( b_{2} is implicative-ideal of X iff ( 0. X in b_{2} & ( for x, y, z being Element of X st (x \ (y \ x)) \ z in b_{2} & z in b_{2} holds

x in b_{2} ) ) );

for X being BCK-algebra

for b

( b

x in b

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 )

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 end;

definition

let X be BCK-algebra;

ex b_{1} being non empty Subset of X st

( 0. X in b_{1} & ( for x, y, z being Element of X st (x \ y) \ z in b_{1} & y \ z in b_{1} holds

x \ z in b_{1} ) )

end;
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 ( 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 ) );

ex b

( 0. X in b

x \ z in b

proof end;

:: deftheorem Def8 defines positive-implicative-ideal BCIIDEAL:def 8 :

for X being BCK-algebra

for b_{2} being non empty Subset of X holds

( b_{2} is positive-implicative-ideal of X iff ( 0. X in b_{2} & ( for x, y, z being Element of X st (x \ y) \ z in b_{2} & y \ z in b_{2} holds

x \ z in b_{2} ) ) );

for X being BCK-algebra

for b

( b

x \ z in b

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 )

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 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

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 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

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 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 )

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 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 )

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 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

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 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 )

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 end;