:: by Tao Sun , Dahai Hu and Xiquan Liang

::

:: Received September 19, 2007

:: Copyright (c) 2007-2012 Association of Mizar Users

begin

definition

let IT be non empty BCIStr_0 ;

end;
attr IT is commutative means :Def1: :: BCIALG_3:def 1

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

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

:: deftheorem Def1 defines commutative BCIALG_3:def 1 :

for IT being non empty BCIStr_0 holds

( IT is commutative iff for x, y being Element of IT holds x \ (x \ y) = y \ (y \ x) );

for IT being non empty BCIStr_0 holds

( IT is commutative iff for x, y being Element of IT holds x \ (x \ y) = y \ (y \ x) );

registration
end;

theorem Th1: :: BCIALG_3:1

for X being BCK-algebra holds

( X is commutative BCK-algebra iff for x, y being Element of X holds x \ (x \ y) <= y \ (y \ x) )

( X is commutative BCK-algebra iff for x, y being Element of X holds x \ (x \ y) <= y \ (y \ x) )

proof end;

theorem Th3: :: BCIALG_3:3

for X being BCK-algebra holds

( X is commutative BCK-algebra iff for x, y being Element of X holds x \ y = x \ (y \ (y \ x)) )

( X is commutative BCK-algebra iff for x, y being Element of X holds x \ y = x \ (y \ (y \ x)) )

proof end;

theorem Th4: :: BCIALG_3:4

for X being BCK-algebra holds

( X is commutative BCK-algebra iff for x, y being Element of X holds x \ (x \ y) = y \ (y \ (x \ (x \ y))) )

( X is commutative BCK-algebra iff for x, y being Element of X holds x \ (x \ y) = y \ (y \ (x \ (x \ y))) )

proof end;

theorem Th5: :: BCIALG_3:5

for X being BCK-algebra holds

( X is commutative BCK-algebra iff for x, y being Element of X st x <= y holds

x = y \ (y \ x) )

( X is commutative BCK-algebra iff for x, y being Element of X st x <= y holds

x = y \ (y \ x) )

proof end;

theorem Th6: :: BCIALG_3:6

for X being non empty BCIStr_0 holds

( X is commutative BCK-algebra iff for x, y, z being Element of X holds

( x \ ((0. X) \ y) = x & (x \ z) \ (x \ y) = (y \ z) \ (y \ x) ) )

( X is commutative BCK-algebra iff for x, y, z being Element of X holds

( x \ ((0. X) \ y) = x & (x \ z) \ (x \ y) = (y \ z) \ (y \ x) ) )

proof end;

theorem :: BCIALG_3:7

for X being BCK-algebra st X is commutative BCK-algebra holds

for x, y being Element of X st x \ y = x holds

y \ x = y

for x, y being Element of X st x \ y = x holds

y \ x = y

proof end;

theorem Th8: :: BCIALG_3:8

for X being BCK-algebra st X is commutative BCK-algebra holds

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

(a \ x) \ (a \ y) = y \ x

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

(a \ x) \ (a \ y) = y \ x

proof end;

theorem :: BCIALG_3:9

for X being BCK-algebra st X is commutative BCK-algebra 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 holds

( x \ y = x iff y \ (y \ x) = 0. X )

proof end;

theorem :: BCIALG_3:10

for X being BCK-algebra st X is commutative BCK-algebra holds

for x, y being Element of X holds

( x \ (y \ (y \ x)) = x \ y & (x \ y) \ ((x \ y) \ x) = x \ y )

for x, y being Element of X holds

( x \ (y \ (y \ x)) = x \ y & (x \ y) \ ((x \ y) \ x) = x \ y )

proof end;

theorem :: BCIALG_3:11

for X being BCK-algebra st X is commutative BCK-algebra holds

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

(a \ y) \ ((a \ y) \ (a \ x)) = (a \ y) \ (x \ y) by Th8;

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

(a \ y) \ ((a \ y) \ (a \ x)) = (a \ y) \ (x \ y) by Th8;

definition

let X be BCI-algebra;

let a be Element of X;

end;
let a be Element of X;

attr a is being_greatest means :Def2: :: BCIALG_3:def 2

for x being Element of X holds x \ a = 0. X;

for x being Element of X holds x \ a = 0. X;

:: deftheorem Def2 defines being_greatest BCIALG_3:def 2 :

for X being BCI-algebra

for a being Element of X holds

( a is being_greatest iff for x being Element of X holds x \ a = 0. X );

for X being BCI-algebra

for a being Element of X holds

( a is being_greatest iff for x being Element of X holds x \ a = 0. X );

:: deftheorem defines being_positive BCIALG_3:def 3 :

for X being BCI-algebra

for a being Element of X holds

( a is being_positive iff (0. X) \ a = 0. X );

for X being BCI-algebra

for a being Element of X holds

( a is being_positive iff (0. X) \ a = 0. X );

begin

definition

let IT be BCI-algebra;

end;
attr IT is BCI-commutative means :Def4: :: BCIALG_3:def 4

for x, y being Element of IT st x \ y = 0. IT holds

x = y \ (y \ x);

for x, y being Element of IT st x \ y = 0. IT holds

x = y \ (y \ x);

:: deftheorem Def4 defines BCI-commutative BCIALG_3:def 4 :

for IT being BCI-algebra holds

( IT is BCI-commutative iff for x, y being Element of IT st x \ y = 0. IT holds

x = y \ (y \ x) );

for IT being BCI-algebra holds

( IT is BCI-commutative iff for x, y being Element of IT st x \ y = 0. IT holds

x = y \ (y \ x) );

:: deftheorem Def5 defines BCI-weakly-commutative BCIALG_3:def 5 :

for IT being BCI-algebra holds

( IT is BCI-weakly-commutative iff for x, y being Element of IT holds (x \ (x \ y)) \ ((0. IT) \ (x \ y)) = y \ (y \ x) );

for IT being BCI-algebra holds

( IT is BCI-weakly-commutative iff for x, y being Element of IT holds (x \ (x \ y)) \ ((0. IT) \ (x \ y)) = y \ (y \ x) );

registration
end;

registration

ex b_{1} being BCI-algebra st

( b_{1} is BCI-commutative & b_{1} is BCI-weakly-commutative )
end;

cluster non empty being_B being_C being_I being_BCI-4 BCI-commutative BCI-weakly-commutative for BCIStr_0 ;

existence ex b

( b

proof end;

theorem :: BCIALG_3:13

for X being BCI-algebra st X is p-Semisimple holds

( X is BCI-commutative & X is BCI-weakly-commutative )

( X is BCI-commutative & X is BCI-weakly-commutative )

proof end;

theorem :: BCIALG_3:14

for X being commutative BCK-algebra holds

( X is BCI-commutative BCI-algebra & X is BCI-weakly-commutative BCI-algebra )

( X is BCI-commutative BCI-algebra & X is BCI-weakly-commutative BCI-algebra )

proof end;

theorem Th16: :: BCIALG_3:16

for X being BCI-algebra holds

( X is BCI-commutative iff for x, y being Element of X holds x \ (x \ y) = y \ (y \ (x \ (x \ y))) )

( X is BCI-commutative iff for x, y being Element of X holds x \ (x \ y) = y \ (y \ (x \ (x \ y))) )

proof end;

theorem Th17: :: BCIALG_3:17

for X being BCI-algebra holds

( X is BCI-commutative iff for x, y being Element of X holds (x \ (x \ y)) \ (y \ (y \ x)) = (0. X) \ (x \ y) )

( X is BCI-commutative iff for x, y being Element of X holds (x \ (x \ y)) \ (y \ (y \ x)) = (0. X) \ (x \ y) )

proof end;

theorem :: BCIALG_3:18

for X being BCI-algebra holds

( X is BCI-commutative iff for a being Element of AtomSet X

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

( X is BCI-commutative iff for a being Element of AtomSet X

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

proof end;

theorem :: BCIALG_3:19

for X being non empty BCIStr_0 holds

( X is BCI-commutative BCI-algebra iff for x, y, z being Element of X holds

( ((x \ y) \ (x \ z)) \ (z \ y) = 0. X & x \ (0. X) = x & x \ (x \ y) = y \ (y \ (x \ (x \ y))) ) )

( X is BCI-commutative BCI-algebra iff for x, y, z being Element of X holds

( ((x \ y) \ (x \ z)) \ (z \ y) = 0. X & x \ (0. X) = x & x \ (x \ y) = y \ (y \ (x \ (x \ y))) ) )

proof end;

theorem :: BCIALG_3:20

for X being BCI-algebra holds

( X is BCI-commutative iff for x, y, z being Element of X st x <= z & z \ y <= z \ x holds

x <= y )

( X is BCI-commutative iff for x, y, z being Element of X st x <= z & z \ y <= z \ x holds

x <= y )

proof end;

theorem :: BCIALG_3:21

for X being BCI-algebra holds

( X is BCI-commutative iff for x, y, z being Element of X st x <= y & x <= z holds

x <= y \ (y \ z) )

( X is BCI-commutative iff for x, y, z being Element of X st x <= y & x <= z holds

x <= y \ (y \ z) )

proof end;

begin

:: deftheorem defines bounded BCIALG_3:def 6 :

for IT being BCK-algebra holds

( IT is bounded iff ex a being Element of IT st a is being_greatest );

for IT being BCK-algebra holds

( IT is bounded iff ex a being Element of IT st a is being_greatest );

registration

ex b_{1} being BCK-algebra st

( b_{1} is bounded & b_{1} is commutative )
end;

cluster non empty being_B being_C being_I being_BCI-4 being_BCK-5 commutative bounded for BCIStr_0 ;

existence ex b

( b

proof end;

definition

let IT be bounded BCK-algebra;

end;
attr IT is involutory means :Def7: :: BCIALG_3:def 7

for a being Element of IT st a is being_greatest holds

for x being Element of IT holds a \ (a \ x) = x;

for a being Element of IT st a is being_greatest holds

for x being Element of IT holds a \ (a \ x) = x;

:: deftheorem Def7 defines involutory BCIALG_3:def 7 :

for IT being bounded BCK-algebra holds

( IT is involutory iff for a being Element of IT st a is being_greatest holds

for x being Element of IT holds a \ (a \ x) = x );

for IT being bounded BCK-algebra holds

( IT is involutory iff for a being Element of IT st a is being_greatest holds

for x being Element of IT holds a \ (a \ x) = x );

theorem Th22: :: BCIALG_3:22

for X being bounded BCK-algebra holds

( X is involutory iff for a being Element of X st a is being_greatest holds

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

( X is involutory iff for a being Element of X st a is being_greatest holds

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

proof end;

theorem Th23: :: BCIALG_3:23

for X being bounded BCK-algebra holds

( X is involutory iff for a being Element of X st a is being_greatest holds

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

( X is involutory iff for a being Element of X st a is being_greatest holds

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

proof end;

theorem :: BCIALG_3:24

for X being bounded BCK-algebra holds

( X is involutory iff for a being Element of X st a is being_greatest holds

for x, y being Element of X st x <= a \ y holds

y <= a \ x )

( X is involutory iff for a being Element of X st a is being_greatest holds

for x, y being Element of X st x <= a \ y holds

y <= a \ x )

proof end;

definition

let IT be BCK-algebra;

let a be Element of IT;

end;
let a be Element of IT;

attr a is being_Iseki means :Def8: :: BCIALG_3:def 8

for x being Element of IT holds

( x \ a = 0. IT & a \ x = a );

for x being Element of IT holds

( x \ a = 0. IT & a \ x = a );

:: deftheorem Def8 defines being_Iseki BCIALG_3:def 8 :

for IT being BCK-algebra

for a being Element of IT holds

( a is being_Iseki iff for x being Element of IT holds

( x \ a = 0. IT & a \ x = a ) );

for IT being BCK-algebra

for a being Element of IT holds

( a is being_Iseki iff for x being Element of IT holds

( x \ a = 0. IT & a \ x = a ) );

:: deftheorem defines Iseki_extension BCIALG_3:def 9 :

for IT being BCK-algebra holds

( IT is Iseki_extension iff ex a being Element of IT st a is being_Iseki );

for IT being BCK-algebra holds

( IT is Iseki_extension iff ex a being Element of IT st a is being_Iseki );

registration
end;

:: Commutative Ideal

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} & z in b_{1} holds

x \ (y \ (y \ x)) in b_{1} ) )

end;
mode Commutative-Ideal of X -> non empty Subset of X means :Def10: :: BCIALG_3:def 10

( 0. X in it & ( for x, y, z being Element of X st (x \ y) \ z in it & z in it holds

x \ (y \ (y \ x)) in it ) );

existence ( 0. X in it & ( for x, y, z being Element of X st (x \ y) \ z in it & z in it holds

x \ (y \ (y \ x)) in it ) );

ex b

( 0. X in b

x \ (y \ (y \ x)) in b

proof end;

:: deftheorem Def10 defines Commutative-Ideal BCIALG_3:def 10 :

for X being BCK-algebra

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

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

x \ (y \ (y \ x)) in b_{2} ) ) );

for X being BCK-algebra

for b

( b

x \ (y \ (y \ x)) in b

theorem :: BCIALG_3:25

for X being BCK-algebra

for IT being non empty Subset of X st IT is Commutative-Ideal of X holds

for x, y being Element of X st x \ y in IT holds

x \ (y \ (y \ x)) in IT

for IT being non empty Subset of X st IT is Commutative-Ideal of X holds

for x, y being Element of X st x \ y in IT holds

x \ (y \ (y \ x)) in IT

proof end;

theorem Th26: :: BCIALG_3:26

for X being BCK-algebra

for IT being non empty Subset of X

for X being BCK-algebra st IT is Commutative-Ideal of X holds

IT is Ideal of X

for IT being non empty Subset of X

for X being BCK-algebra st IT is Commutative-Ideal of X holds

IT is Ideal of X

proof end;

theorem :: BCIALG_3:27

for X being BCK-algebra

for IT being non empty Subset of X st IT is Commutative-Ideal of X holds

for x, y being Element of X st x \ (x \ y) in IT holds

(y \ (y \ x)) \ (x \ y) in IT

for IT being non empty Subset of X st IT is Commutative-Ideal of X holds

for x, y being Element of X st x \ (x \ y) in IT holds

(y \ (y \ x)) \ (x \ y) in IT

proof end;

begin

definition

let IT be BCK-algebra;

end;
attr IT is BCK-positive-implicative means :Def11: :: BCIALG_3:def 11

for x, y, z being Element of IT holds (x \ y) \ z = (x \ z) \ (y \ z);

for x, y, z being Element of IT holds (x \ y) \ z = (x \ z) \ (y \ z);

attr IT is BCK-implicative means :Def12: :: BCIALG_3:def 12

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

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

:: deftheorem Def11 defines BCK-positive-implicative BCIALG_3:def 11 :

for IT being BCK-algebra holds

( IT is BCK-positive-implicative iff for x, y, z being Element of IT holds (x \ y) \ z = (x \ z) \ (y \ z) );

for IT being BCK-algebra holds

( IT is BCK-positive-implicative iff for x, y, z being Element of IT holds (x \ y) \ z = (x \ z) \ (y \ z) );

:: deftheorem Def12 defines BCK-implicative BCIALG_3:def 12 :

for IT being BCK-algebra holds

( IT is BCK-implicative iff for x, y being Element of IT holds x \ (y \ x) = x );

for IT being BCK-algebra holds

( IT is BCK-implicative iff for x, y being Element of IT holds x \ (y \ x) = x );

registration
end;

registration

ex b_{1} being BCK-algebra st

( b_{1} is Iseki_extension & b_{1} is BCK-positive-implicative & b_{1} is BCK-implicative & b_{1} is bounded & b_{1} is commutative )
end;

cluster non empty being_B being_C being_I being_BCI-4 being_BCK-5 commutative bounded Iseki_extension BCK-positive-implicative BCK-implicative for BCIStr_0 ;

existence ex b

( b

proof end;

theorem Th28: :: BCIALG_3:28

for X being BCK-algebra holds

( X is BCK-positive-implicative BCK-algebra iff for x, y being Element of X holds x \ y = (x \ y) \ y )

( X is BCK-positive-implicative BCK-algebra iff for x, y being Element of X holds x \ y = (x \ y) \ y )

proof end;

theorem Th29: :: BCIALG_3:29

for X being BCK-algebra holds

( X is BCK-positive-implicative BCK-algebra iff for x, y being Element of X holds (x \ (x \ y)) \ (y \ x) = x \ (x \ (y \ (y \ x))) )

( X is BCK-positive-implicative BCK-algebra iff for x, y being Element of X holds (x \ (x \ y)) \ (y \ x) = x \ (x \ (y \ (y \ x))) )

proof end;

theorem :: BCIALG_3:30

for X being BCK-algebra holds

( X is BCK-positive-implicative BCK-algebra iff for x, y being Element of X holds x \ y = (x \ y) \ (x \ (x \ y)) )

( X is BCK-positive-implicative BCK-algebra iff for x, y being Element of X holds x \ y = (x \ y) \ (x \ (x \ y)) )

proof end;

theorem :: BCIALG_3:31

for X being BCK-algebra holds

( X is BCK-positive-implicative BCK-algebra iff for x, y, z being Element of X holds (x \ z) \ (y \ z) <= (x \ y) \ z )

( X is BCK-positive-implicative BCK-algebra iff for x, y, z being Element of X holds (x \ z) \ (y \ z) <= (x \ y) \ z )

proof end;

theorem :: BCIALG_3:32

for X being BCK-algebra holds

( X is BCK-positive-implicative BCK-algebra iff for x, y being Element of X holds x \ y <= (x \ y) \ y )

( X is BCK-positive-implicative BCK-algebra iff for x, y being Element of X holds x \ y <= (x \ y) \ y )

proof end;

theorem :: BCIALG_3:33

for X being BCK-algebra holds

( X is BCK-positive-implicative BCK-algebra iff for x, y being Element of X holds x \ (x \ (y \ (y \ x))) <= (x \ (x \ y)) \ (y \ x) )

( X is BCK-positive-implicative BCK-algebra iff for x, y being Element of X holds x \ (x \ (y \ (y \ x))) <= (x \ (x \ y)) \ (y \ x) )

proof end;

theorem Th34: :: BCIALG_3:34

for X being BCK-algebra holds

( X is BCK-implicative BCK-algebra iff ( X is commutative BCK-algebra & X is BCK-positive-implicative BCK-algebra ) )

( X is BCK-implicative BCK-algebra iff ( X is commutative BCK-algebra & X is BCK-positive-implicative BCK-algebra ) )

proof end;

theorem Th35: :: BCIALG_3:35

for X being BCK-algebra holds

( X is BCK-implicative BCK-algebra iff for x, y being Element of X holds (x \ (x \ y)) \ (x \ y) = y \ (y \ x) )

( X is BCK-implicative BCK-algebra iff for x, y being Element of X holds (x \ (x \ y)) \ (x \ y) = y \ (y \ x) )

proof end;

theorem :: BCIALG_3:36

for X being non empty BCIStr_0 holds

( X is BCK-implicative BCK-algebra iff for x, y, z being Element of X holds

( x \ ((0. X) \ y) = x & (x \ z) \ (x \ y) = ((y \ z) \ (y \ x)) \ (x \ y) ) )

( X is BCK-implicative BCK-algebra iff for x, y, z being Element of X holds

( x \ ((0. X) \ y) = x & (x \ z) \ (x \ y) = ((y \ z) \ (y \ x)) \ (x \ y) ) )

proof end;

Lm1: for X being bounded BCK-algebra st X is BCK-implicative holds

for a being Element of X st a is being_greatest holds

for x being Element of X holds a \ (a \ x) = x

proof end;

theorem Th37: :: BCIALG_3:37

for X being bounded BCK-algebra

for a being Element of X st a is being_greatest holds

( X is BCK-implicative iff ( X is involutory & X is BCK-positive-implicative ) )

for a being Element of X st a is being_greatest holds

( X is BCK-implicative iff ( X is involutory & X is BCK-positive-implicative ) )

proof end;

theorem :: BCIALG_3:38

for X being BCK-algebra holds

( X is BCK-implicative BCK-algebra iff for x, y being Element of X holds x \ (x \ (y \ x)) = 0. X )

( X is BCK-implicative BCK-algebra iff for x, y being Element of X holds x \ (x \ (y \ x)) = 0. X )

proof end;

theorem :: BCIALG_3:39

for X being BCK-algebra holds

( X is BCK-implicative BCK-algebra iff for x, y being Element of X holds (x \ (x \ y)) \ (x \ y) = y \ (y \ (x \ (x \ y))) )

( X is BCK-implicative BCK-algebra iff for x, y being Element of X holds (x \ (x \ y)) \ (x \ y) = y \ (y \ (x \ (x \ y))) )

proof end;

theorem Th40: :: BCIALG_3:40

for X being BCK-algebra holds

( X is BCK-implicative BCK-algebra iff for x, y, z being Element of X holds (x \ z) \ (x \ y) = (y \ z) \ ((y \ x) \ z) )

( X is BCK-implicative BCK-algebra iff for x, y, z being Element of X holds (x \ z) \ (x \ y) = (y \ z) \ ((y \ x) \ z) )

proof end;

theorem :: BCIALG_3:41

for X being BCK-algebra holds

( X is BCK-implicative BCK-algebra iff for x, y, z being Element of X holds x \ (x \ (y \ z)) = (y \ z) \ ((y \ z) \ (x \ z)) )

( X is BCK-implicative BCK-algebra iff for x, y, z being Element of X holds x \ (x \ (y \ z)) = (y \ z) \ ((y \ z) \ (x \ z)) )

proof end;

theorem :: BCIALG_3:42

for X being BCK-algebra holds

( X is BCK-implicative BCK-algebra iff for x, y being Element of X holds x \ (x \ y) = (y \ (y \ x)) \ (x \ y) )

( X is BCK-implicative BCK-algebra iff for x, y being Element of X holds x \ (x \ y) = (y \ (y \ x)) \ (x \ y) )

proof end;

theorem Th43: :: BCIALG_3:43

for X being commutative bounded BCK-algebra

for a being Element of X st a is being_greatest holds

( X is BCK-implicative iff for x being Element of X holds (a \ x) \ ((a \ x) \ x) = 0. X )

for a being Element of X st a is being_greatest holds

( X is BCK-implicative iff for x being Element of X holds (a \ x) \ ((a \ x) \ x) = 0. X )

proof end;

theorem :: BCIALG_3:44

for X being commutative bounded BCK-algebra

for a being Element of X st a is being_greatest holds

( X is BCK-implicative iff for x being Element of X holds x \ (a \ x) = x )

for a being Element of X st a is being_greatest holds

( X is BCK-implicative iff for x being Element of X holds x \ (a \ x) = x )

proof end;

theorem :: BCIALG_3:45

for X being commutative bounded BCK-algebra

for a being Element of X st a is being_greatest holds

( X is BCK-implicative iff for x being Element of X holds (a \ x) \ x = a \ x )

for a being Element of X st a is being_greatest holds

( X is BCK-implicative iff for x being Element of X holds (a \ x) \ x = a \ x )

proof end;

theorem Th46: :: BCIALG_3:46

for X being commutative bounded BCK-algebra

for a being Element of X st a is being_greatest holds

( X is BCK-implicative iff for x, y being Element of X holds (a \ y) \ ((a \ y) \ x) = x \ y )

for a being Element of X st a is being_greatest holds

( X is BCK-implicative iff for x, y being Element of X holds (a \ y) \ ((a \ y) \ x) = x \ y )

proof end;

theorem Th47: :: BCIALG_3:47

for X being commutative bounded BCK-algebra

for a being Element of X st a is being_greatest holds

( X is BCK-implicative iff for x, y being Element of X holds y \ (y \ x) = x \ (a \ y) )

for a being Element of X st a is being_greatest holds

( X is BCK-implicative iff for x, y being Element of X holds y \ (y \ x) = x \ (a \ y) )

proof end;

theorem :: BCIALG_3:48

for X being commutative bounded BCK-algebra

for a being Element of X st a is being_greatest holds

( X is BCK-implicative iff for x, y, z being Element of X holds (x \ (y \ z)) \ (x \ y) <= x \ (a \ z) )

for a being Element of X st a is being_greatest holds

( X is BCK-implicative iff for x, y, z being Element of X holds (x \ (y \ z)) \ (x \ y) <= x \ (a \ z) )

proof end;