:: Several Classes of {BCI}-algebras and Their Properties
:: by Yuzhong Ding
::
:: Copyright (c) 2007-2021 Association of Mizar Users

definition
attr c1 is strict ;
struct BCIStr -> 1-sorted ;
aggr BCIStr(# carrier, InternalDiff #) -> BCIStr ;
sel InternalDiff c1 -> BinOp of the carrier of c1;
end;

registration
cluster non empty strict for BCIStr ;
existence
ex b1 being BCIStr st
( not b1 is empty & b1 is strict )
proof end;
end;

definition
let A be BCIStr ;
let x, y be Element of A;
func x \ y -> Element of A equals :: BCIALG_1:def 1
the InternalDiff of A . (x,y);
coherence
the InternalDiff of A . (x,y) is Element of A
;
end;

:: deftheorem defines \ BCIALG_1:def 1 :
for A being BCIStr
for x, y being Element of A holds x \ y = the InternalDiff of A . (x,y);

definition end;

registration
cluster non empty strict for BCIStr_0 ;
existence
ex b1 being BCIStr_0 st
( not b1 is empty & b1 is strict )
proof end;
end;

definition
let IT be non empty BCIStr_0 ;
let x be Element of IT;
func x  -> Element of IT equals :: BCIALG_1:def 2
(0. IT) \ x;
coherence
(0. IT) \ x is Element of IT
;
end;

:: deftheorem defines  BCIALG_1:def 2 :
for IT being non empty BCIStr_0
for x being Element of IT holds x  = (0. IT) \ x;

definition
let IT be non empty BCIStr_0 ;
attr IT is being_B means :Def3: :: BCIALG_1:def 3
for x, y, z being Element of IT holds ((x \ y) \ (z \ y)) \ (x \ z) = 0. IT;
attr IT is being_C means :Def4: :: BCIALG_1:def 4
for x, y, z being Element of IT holds ((x \ y) \ z) \ ((x \ z) \ y) = 0. IT;
attr IT is being_I means :Def5: :: BCIALG_1:def 5
for x being Element of IT holds x \ x = 0. IT;
attr IT is being_K means :: BCIALG_1:def 6
for x, y being Element of IT holds (x \ y) \ x = 0. IT;
attr IT is being_BCI-4 means :Def7: :: BCIALG_1:def 7
for x, y being Element of IT st x \ y = 0. IT & y \ x = 0. IT holds
x = y;
attr IT is being_BCK-5 means :Def8: :: BCIALG_1:def 8
for x being Element of IT holds x  = 0. IT;
end;

:: deftheorem Def3 defines being_B BCIALG_1:def 3 :
for IT being non empty BCIStr_0 holds
( IT is being_B iff for x, y, z being Element of IT holds ((x \ y) \ (z \ y)) \ (x \ z) = 0. IT );

:: deftheorem Def4 defines being_C BCIALG_1:def 4 :
for IT being non empty BCIStr_0 holds
( IT is being_C iff for x, y, z being Element of IT holds ((x \ y) \ z) \ ((x \ z) \ y) = 0. IT );

:: deftheorem Def5 defines being_I BCIALG_1:def 5 :
for IT being non empty BCIStr_0 holds
( IT is being_I iff for x being Element of IT holds x \ x = 0. IT );

:: deftheorem defines being_K BCIALG_1:def 6 :
for IT being non empty BCIStr_0 holds
( IT is being_K iff for x, y being Element of IT holds (x \ y) \ x = 0. IT );

:: deftheorem Def7 defines being_BCI-4 BCIALG_1:def 7 :
for IT being non empty BCIStr_0 holds
( IT is being_BCI-4 iff for x, y being Element of IT st x \ y = 0. IT & y \ x = 0. IT holds
x = y );

:: deftheorem Def8 defines being_BCK-5 BCIALG_1:def 8 :
for IT being non empty BCIStr_0 holds
( IT is being_BCK-5 iff for x being Element of IT holds x  = 0. IT );

definition
func BCI-EXAMPLE -> BCIStr_0 equals :: BCIALG_1:def 9
BCIStr_0(# ,op2,op0 #);
coherence
BCIStr_0(# ,op2,op0 #) is BCIStr_0
;
end;

:: deftheorem defines BCI-EXAMPLE BCIALG_1:def 9 :

registration
coherence
( BCI-EXAMPLE is strict & BCI-EXAMPLE is 1 -element )
;
end;

registration
coherence by STRUCT_0:def 10;
end;

registration
existence
ex b1 being non empty BCIStr_0 st
( b1 is strict & b1 is being_B & b1 is being_C & b1 is being_I & b1 is being_BCI-4 & b1 is being_BCK-5 )
proof end;
end;

definition end;

definition end;

definition
let X be BCI-algebra;
mode SubAlgebra of X -> BCI-algebra means :Def10: :: BCIALG_1:def 10
( 0. it = 0. X & the carrier of it c= the carrier of X & the InternalDiff of it = the InternalDiff of X || the carrier of it );
existence
ex b1 being BCI-algebra st
( 0. b1 = 0. X & the carrier of b1 c= the carrier of X & the InternalDiff of b1 = the InternalDiff of X || the carrier of b1 )
proof end;
end;

:: deftheorem Def10 defines SubAlgebra BCIALG_1:def 10 :
for X, b2 being BCI-algebra holds
( b2 is SubAlgebra of X iff ( 0. b2 = 0. X & the carrier of b2 c= the carrier of X & the InternalDiff of b2 = the InternalDiff of X || the carrier of b2 ) );

::T1.1.11
theorem Th1: :: BCIALG_1:1
for X being non empty BCIStr_0 holds
( X is BCI-algebra iff ( X is being_I & X is being_BCI-4 & ( for x, y, z being Element of X holds
( ((x \ y) \ (x \ z)) \ (z \ y) = 0. X & (x \ (x \ y)) \ y = 0. X ) ) ) )
proof end;

definition
let IT be non empty BCIStr_0 ;
let x, y be Element of IT;
pred x <= y means :: BCIALG_1:def 11
x \ y = 0. IT;
end;

:: deftheorem defines <= BCIALG_1:def 11 :
for IT being non empty BCIStr_0
for x, y being Element of IT holds
( x <= y iff x \ y = 0. IT );

Lm1: for X being BCI-algebra
for x being Element of X st x \ (0. X) = 0. X holds
x = 0. X

proof end;

theorem Th2: :: BCIALG_1:2
for X being BCI-algebra
for x being Element of X holds x \ (0. X) = x
proof end;

theorem Th3: :: BCIALG_1:3
for X being BCI-algebra
for x, y, z being Element of X st x \ y = 0. X & y \ z = 0. X holds
x \ z = 0. X
proof end;

theorem Th4: :: BCIALG_1:4
for X being BCI-algebra
for x, y, z being Element of X st x \ y = 0. X holds
( (x \ z) \ (y \ z) = 0. X & (z \ y) \ (z \ x) = 0. X )
proof end;

theorem :: BCIALG_1:5
for X being BCI-algebra
for x, y, z being Element of X st x <= y holds
( x \ z <= y \ z & z \ y <= z \ x ) by Th4;

theorem :: BCIALG_1:6
for X being BCI-algebra
for x, y being Element of X st x \ y = 0. X holds
(y \ x)  = 0. X
proof end;

theorem Th7: :: BCIALG_1:7
for X being BCI-algebra
for x, y, z being Element of X holds (x \ y) \ z = (x \ z) \ y
proof end;

theorem Th8: :: BCIALG_1:8
for X being BCI-algebra
for x, y being Element of X holds x \ (x \ (x \ y)) = x \ y
proof end;

theorem Th9: :: BCIALG_1:9
for X being BCI-algebra
for x, y being Element of X holds (x \ y)  = (x ) \ (y )
proof end;

theorem Th10: :: BCIALG_1:10
for X being BCI-algebra
for x, y being Element of X holds ((x \ (x \ y)) \ (y \ x)) \ (x \ (x \ (y \ (y \ x)))) = 0. X
proof end;

theorem :: BCIALG_1:11
for X being non empty BCIStr_0 holds
( X is BCI-algebra iff ( X is being_BCI-4 & ( for x, y, z being Element of X holds
( ((x \ y) \ (x \ z)) \ (z \ y) = 0. X & x \ (0. X) = x ) ) ) )
proof end;

theorem :: BCIALG_1:12
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
X is BCK-algebra
proof end;

theorem :: BCIALG_1:13
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
X is BCK-algebra
proof end;

theorem :: BCIALG_1:14
for X being BCI-algebra st ( for X being BCI-algebra
for x, y being Element of X holds x \ (y \ x) = x ) holds
X is BCK-algebra
proof end;

theorem :: BCIALG_1:15
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
X is BCK-algebra
proof end;

theorem :: BCIALG_1:16
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
X is BCK-algebra
proof end;

theorem :: BCIALG_1:17
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
X is BCK-algebra
proof end;

theorem :: BCIALG_1:18
for X being BCI-algebra holds
( X is being_K iff X is BCK-algebra )
proof end;

definition
let X be BCI-algebra;
func BCK-part X -> non empty Subset of X equals :: BCIALG_1:def 12
{ x where x is Element of X : 0. X <= x } ;
coherence
{ x where x is Element of X : 0. X <= x } is non empty Subset of X
proof end;
end;

:: deftheorem defines BCK-part BCIALG_1:def 12 :
for X being BCI-algebra holds BCK-part X = { x where x is Element of X : 0. X <= x } ;

theorem Th19: :: BCIALG_1:19
for X being BCI-algebra holds 0. X in BCK-part X
proof end;

theorem :: BCIALG_1:20
for X being BCI-algebra
for x, y being Element of BCK-part X holds x \ y in BCK-part X
proof end;

theorem :: BCIALG_1:21
for X being BCI-algebra
for x being Element of X
for y being Element of BCK-part X holds x \ y <= x
proof end;

theorem Th22: :: BCIALG_1:22
for X being BCI-algebra holds X is SubAlgebra of X
proof end;

definition
let X be BCI-algebra;
let IT be SubAlgebra of X;
attr IT is proper means :Def13: :: BCIALG_1:def 13
IT <> X;
end;

:: deftheorem Def13 defines proper BCIALG_1:def 13 :
for X being BCI-algebra
for IT being SubAlgebra of X holds
( IT is proper iff IT <> X );

registration
let X be BCI-algebra;
existence
not for b1 being SubAlgebra of X holds b1 is proper
proof end;
end;

definition
let X be BCI-algebra;
let IT be Element of X;
attr IT is atom means :: BCIALG_1:def 14
for z being Element of X st z \ IT = 0. X holds
z = IT;
end;

:: deftheorem defines atom BCIALG_1:def 14 :
for X being BCI-algebra
for IT being Element of X holds
( IT is atom iff for z being Element of X st z \ IT = 0. X holds
z = IT );

definition
let X be BCI-algebra;
func AtomSet X -> non empty Subset of X equals :: BCIALG_1:def 15
{ x where x is Element of X : x is atom } ;
coherence
{ x where x is Element of X : x is atom } is non empty Subset of X
proof end;
end;

:: deftheorem defines AtomSet BCIALG_1:def 15 :
for X being BCI-algebra holds AtomSet X = { x where x is Element of X : x is atom } ;

theorem Th23: :: BCIALG_1:23
for X being BCI-algebra holds 0. X in AtomSet X
proof end;

theorem Th24: :: BCIALG_1:24
for X being BCI-algebra
for x being Element of X holds
( x in AtomSet X iff for z being Element of X holds z \ (z \ x) = x )
proof end;

theorem :: BCIALG_1:25
for X being BCI-algebra
for x being Element of X holds
( x in AtomSet X iff for u, z being Element of X holds (z \ u) \ (z \ x) = x \ u )
proof end;

theorem :: BCIALG_1:26
for X being BCI-algebra
for x being Element of X holds
( x in AtomSet X iff for y, z being Element of X holds x \ (z \ y) <= y \ (z \ x) )
proof end;

theorem :: BCIALG_1:27
for X being BCI-algebra
for x being Element of X holds
( x in AtomSet X iff for y, z, u being Element of X holds (x \ u) \ (z \ y) <= (y \ u) \ (z \ x) )
proof end;

theorem Th28: :: BCIALG_1:28
for X being BCI-algebra
for x being Element of X holds
( x in AtomSet X iff for z being Element of X holds (z ) \ (x ) = x \ z )
proof end;

theorem Th29: :: BCIALG_1:29
for X being BCI-algebra
for x being Element of X holds
( x in AtomSet X iff (x )  = x )
proof end;

theorem Th30: :: BCIALG_1:30
for X being BCI-algebra
for x being Element of X holds
( x in AtomSet X iff for z being Element of X holds (z \ x)  = x \ z )
proof end;

theorem Th31: :: BCIALG_1:31
for X being BCI-algebra
for x being Element of X holds
( x in AtomSet X iff for z being Element of X holds ((x \ z) )  = x \ z )
proof end;

theorem :: BCIALG_1:32
for X being BCI-algebra
for x being Element of X holds
( x in AtomSet X iff for z, u being Element of X holds z \ (z \ (x \ u)) = x \ u )
proof end;

theorem Th33: :: BCIALG_1:33
for X being BCI-algebra
for a being Element of AtomSet X
for x being Element of X holds a \ x in AtomSet X
proof end;

definition
let X be BCI-algebra;
let a, b be Element of AtomSet X;
:: original: \
redefine func a \ b -> Element of AtomSet X;
coherence
a \ b is Element of AtomSet X
by Th33;
end;

theorem Th34: :: BCIALG_1:34
for X being BCI-algebra
for x being Element of X holds x  in AtomSet X
proof end;

theorem Th35: :: BCIALG_1:35
for X being BCI-algebra
for x being Element of X ex a being Element of AtomSet X st a <= x
proof end;

definition
let X be BCI-algebra;
attr X is generated_by_atom means :: BCIALG_1:def 16
for x being Element of X ex a being Element of AtomSet X st a <= x;
end;

:: deftheorem defines generated_by_atom BCIALG_1:def 16 :
for X being BCI-algebra holds
( X is generated_by_atom iff for x being Element of X ex a being Element of AtomSet X st a <= x );

definition
let X be BCI-algebra;
let a be Element of AtomSet X;
func BranchV a -> non empty Subset of X equals :: BCIALG_1:def 17
{ x where x is Element of X : a <= x } ;
coherence
{ x where x is Element of X : a <= x } is non empty Subset of X
proof end;
end;

:: deftheorem defines BranchV BCIALG_1:def 17 :
for X being BCI-algebra
for a being Element of AtomSet X holds BranchV a = { x where x is Element of X : a <= x } ;

theorem :: BCIALG_1:36
for X being BCI-algebra holds X is generated_by_atom by Th35;

theorem :: BCIALG_1:37
for X being BCI-algebra
for a, b being Element of AtomSet X
for x being Element of BranchV b holds a \ x = a \ b
proof end;

theorem Th38: :: BCIALG_1:38
for X being BCI-algebra
for a being Element of AtomSet X
for x being Element of BCK-part X holds a \ x = a
proof end;

Lm2: for X being BCI-algebra
for a being Element of AtomSet X
for x being Element of BranchV a holds a \ x = 0. X

proof end;

theorem Th39: :: BCIALG_1:39
for X being BCI-algebra
for a, b being Element of AtomSet X
for x being Element of BranchV a
for y being Element of BranchV b holds x \ y in BranchV (a \ b)
proof end;

theorem :: BCIALG_1:40
for X being BCI-algebra
for a being Element of AtomSet X
for x, y being Element of BranchV a holds x \ y in BCK-part X
proof end;

theorem :: BCIALG_1:41
for X being BCI-algebra
for a, b being Element of AtomSet X
for x being Element of BranchV a
for y being Element of BranchV b st a <> b holds
not x \ y in BCK-part X
proof end;

theorem :: BCIALG_1:42
for X being BCI-algebra
for a, b being Element of AtomSet X st a <> b holds
() /\ () = {}
proof end;

::Ideal
definition
let X be BCI-algebra;
mode Ideal of X -> non empty Subset of X means :Def18: :: BCIALG_1:def 18
( 0. X in it & ( for x, y being Element of X st x \ y 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 being Element of X st x \ y in b1 & y in b1 holds
x in b1 ) )
proof end;
end;

:: deftheorem Def18 defines Ideal BCIALG_1:def 18 :
for X being BCI-algebra
for b2 being non empty Subset of X holds
( b2 is Ideal of X iff ( 0. X in b2 & ( for x, y being Element of X st x \ y in b2 & y in b2 holds
x in b2 ) ) );

definition
let X be BCI-algebra;
let IT be Ideal of X;
attr IT is closed means :Def19: :: BCIALG_1:def 19
for x being Element of IT holds x  in IT;
end;

:: deftheorem Def19 defines closed BCIALG_1:def 19 :
for X being BCI-algebra
for IT being Ideal of X holds
( IT is closed iff for x being Element of IT holds x  in IT );

Lm3: for X being BCI-algebra holds {(0. X)} is Ideal of X
proof end;

Lm4: for X being BCI-algebra
for X1 being Ideal of X st X1 = {(0. X)} holds
for x being Element of X1 holds x  in {(0. X)}

proof end;

registration
let X be BCI-algebra;
cluster non empty closed for Ideal of X;
existence
ex b1 being Ideal of X st b1 is closed
proof end;
end;

theorem :: BCIALG_1:43
for X being BCI-algebra holds {(0. X)} is closed Ideal of X
proof end;

theorem :: BCIALG_1:44
for X being BCI-algebra holds the carrier of X is closed Ideal of X
proof end;

theorem :: BCIALG_1:45
for X being BCI-algebra holds BCK-part X is closed Ideal of X
proof end;

Lm5: for X being BCI-algebra
for IT being non empty Subset of X st IT is Ideal of X holds
for x, y being Element of IT holds { z where z is Element of X : z \ x <= y } c= IT

proof end;

theorem :: BCIALG_1:46
for X being BCI-algebra
for IT being non empty Subset of X st IT is Ideal of X holds
for x, y being Element of X st x in IT & y <= x holds
y in IT
proof end;

definition
let IT be BCI-algebra;
attr IT is associative means :Def20: :: BCIALG_1:def 20
for x, y, z being Element of IT holds (x \ y) \ z = x \ (y \ z);
attr IT is quasi-associative means :: BCIALG_1:def 21
for x being Element of IT holds (x )  = x  ;
attr IT is positive-implicative means :: BCIALG_1:def 22
for x, y being Element of IT holds (x \ (x \ y)) \ (y \ x) = x \ (x \ (y \ (y \ x)));
attr IT is weakly-positive-implicative means :Def23: :: BCIALG_1:def 23
for x, y, z being Element of IT holds (x \ y) \ z = ((x \ z) \ z) \ (y \ z);
attr IT is implicative means :Def24: :: BCIALG_1:def 24
for x, y being Element of IT holds (x \ (x \ y)) \ (y \ x) = y \ (y \ x);
attr IT is weakly-implicative means :: BCIALG_1:def 25
for x, y being Element of IT holds (x \ (y \ x)) \ ((y \ x) ) = x;
attr IT is p-Semisimple means :Def26: :: BCIALG_1:def 26
for x, y being Element of IT holds x \ (x \ y) = y;
attr IT is alternative means :: BCIALG_1:def 27
for x, y being Element of IT holds
( x \ (x \ y) = (x \ x) \ y & (x \ y) \ y = x \ (y \ y) );
end;

:: deftheorem Def20 defines associative BCIALG_1:def 20 :
for IT being BCI-algebra holds
( IT is associative iff for x, y, z being Element of IT holds (x \ y) \ z = x \ (y \ z) );

:: deftheorem defines quasi-associative BCIALG_1:def 21 :
for IT being BCI-algebra holds
( IT is quasi-associative iff for x being Element of IT holds (x )  = x  );

:: deftheorem defines positive-implicative BCIALG_1:def 22 :
for IT being BCI-algebra holds
( IT is positive-implicative iff for x, y being Element of IT holds (x \ (x \ y)) \ (y \ x) = x \ (x \ (y \ (y \ x))) );

:: deftheorem Def23 defines weakly-positive-implicative BCIALG_1:def 23 :
for IT being BCI-algebra holds
( IT is weakly-positive-implicative iff for x, y, z being Element of IT holds (x \ y) \ z = ((x \ z) \ z) \ (y \ z) );

:: deftheorem Def24 defines implicative BCIALG_1:def 24 :
for IT being BCI-algebra holds
( IT is implicative iff for x, y being Element of IT holds (x \ (x \ y)) \ (y \ x) = y \ (y \ x) );

:: deftheorem defines weakly-implicative BCIALG_1:def 25 :
for IT being BCI-algebra holds
( IT is weakly-implicative iff for x, y being Element of IT holds (x \ (y \ x)) \ ((y \ x) ) = x );

:: deftheorem Def26 defines p-Semisimple BCIALG_1:def 26 :
for IT being BCI-algebra holds
( IT is p-Semisimple iff for x, y being Element of IT holds x \ (x \ y) = y );

:: deftheorem defines alternative BCIALG_1:def 27 :
for IT being BCI-algebra holds
( IT is alternative iff for x, y being Element of IT holds
( x \ (x \ y) = (x \ x) \ y & (x \ y) \ y = x \ (y \ y) ) );

registration
coherence by STRUCT_0:def 10;
end;

registration
existence
ex b1 being BCI-algebra st
( b1 is implicative & b1 is positive-implicative & b1 is p-Semisimple & b1 is associative & b1 is weakly-implicative & b1 is weakly-positive-implicative )
proof end;
end;

Lm6: for X being BCI-algebra st ( for x, y being Element of X holds y \ x = x \ y ) holds
X is associative

proof end;

Lm7: for X being BCI-algebra st ( for x being Element of X holds x  = x ) holds
for x, y being Element of X holds x \ y = y \ x

proof end;

theorem Th47: :: BCIALG_1:47
for X being BCI-algebra holds
( X is associative iff for x being Element of X holds x  = x )
proof end;

theorem Th48: :: BCIALG_1:48
for X being BCI-algebra holds
( ( for x, y being Element of X holds y \ x = x \ y ) iff X is associative )
proof end;

theorem Th49: :: BCIALG_1:49
for X being non empty BCIStr_0 holds
( X is associative BCI-algebra iff for x, y, z being Element of X holds
( (y \ x) \ (z \ x) = z \ y & x \ (0. X) = x ) )
proof end;

theorem Th50: :: BCIALG_1:50
for X being non empty BCIStr_0 holds
( X is associative BCI-algebra iff for x, y, z being Element of X holds
( (x \ y) \ (x \ z) = z \ y & x  = x ) )
proof end;

theorem :: BCIALG_1:51
for X being non empty BCIStr_0 holds
( X is associative BCI-algebra iff for x, y, z being Element of X holds
( (x \ y) \ (x \ z) = y \ z & x \ (0. X) = x ) )
proof end;

theorem :: BCIALG_1:52
for X being BCI-algebra holds
( X is p-Semisimple iff for x being Element of X holds x is atom )
proof end;

theorem :: BCIALG_1:53
for X being BCI-algebra st X is p-Semisimple holds
BCK-part X = {(0. X)}
proof end;

Lm8: for X being BCI-algebra holds
( ( for x, y being Element of X holds y \ (y \ x) = x ) iff for x, y, z being Element of X holds (z \ y) \ (z \ x) = x \ y )

proof end;

theorem Th54: :: BCIALG_1:54
for X being BCI-algebra holds
( X is p-Semisimple iff for x being Element of X holds (x )  = x )
proof end;

theorem :: BCIALG_1:55
for X being BCI-algebra holds
( X is p-Semisimple iff for x, y being Element of X holds y \ (y \ x) = x ) ;

theorem Th56: :: BCIALG_1:56
for X being BCI-algebra holds
( X is p-Semisimple iff for x, y, z being Element of X holds (z \ y) \ (z \ x) = x \ y )
proof end;

theorem Th57: :: BCIALG_1:57
for X being BCI-algebra holds
( X is p-Semisimple iff for x, y, z being Element of X holds x \ (z \ y) = y \ (z \ x) )
proof end;

Lm9: for X being BCI-algebra st X is p-Semisimple holds
for x, y, z, u being Element of X holds
( (x \ u) \ (z \ y) = (y \ u) \ (z \ x) & (x \ u) \ (z \ y) = (x \ z) \ (u \ y) )

proof end;

Lm10: for X being BCI-algebra st X is p-Semisimple holds
for x, y being Element of X holds (y ) \ ((0. X) \ x) = x \ y

proof end;

Lm11: for X being BCI-algebra st X is p-Semisimple holds
for x, y, z being Element of X holds (x \ y) \ (z \ y) = x \ z

proof end;

Lm12: for X being BCI-algebra st X is p-Semisimple holds
for x, y, z being Element of X st x \ y = x \ z holds
y = z

proof end;

Lm13: for X being BCI-algebra st X is p-Semisimple holds
for x, y, z being Element of X holds x \ (y \ z) = (z \ y) \ (x )

proof end;

Lm14: for X being BCI-algebra st X is p-Semisimple holds
for x, y, z being Element of X st y \ x = z \ x holds
y = z

proof end;

theorem :: BCIALG_1:58
for X being BCI-algebra holds
( X is p-Semisimple iff for x, y, z, u being Element of X holds (x \ u) \ (z \ y) = (y \ u) \ (z \ x) )
proof end;

theorem Th59: :: BCIALG_1:59
for X being BCI-algebra holds
( X is p-Semisimple iff for x, z being Element of X holds (z ) \ (x ) = x \ z )
proof end;

theorem :: BCIALG_1:60
for X being BCI-algebra holds
( X is p-Semisimple iff for x, z being Element of X holds ((x \ z) )  = x \ z )
proof end;

theorem :: BCIALG_1:61
for X being BCI-algebra holds
( X is p-Semisimple iff for x, u, z being Element of X holds z \ (z \ (x \ u)) = x \ u )
proof end;

theorem Th62: :: BCIALG_1:62
for X being BCI-algebra holds
( X is p-Semisimple iff for x being Element of X st x  = 0. X holds
x = 0. X )
proof end;

theorem Th63: :: BCIALG_1:63
for X being BCI-algebra holds
( X is p-Semisimple iff for x, y being Element of X holds x \ (y ) = y \ (x ) )
proof end;

theorem :: BCIALG_1:64
for X being BCI-algebra holds
( X is p-Semisimple iff for x, y, z, u being Element of X holds (x \ y) \ (z \ u) = (x \ z) \ (y \ u) )
proof end;

theorem :: BCIALG_1:65
for X being BCI-algebra holds
( X is p-Semisimple iff for x, y, z being Element of X holds (x \ y) \ (z \ y) = x \ z )
proof end;

theorem :: BCIALG_1:66
for X being BCI-algebra holds
( X is p-Semisimple iff for x, y, z being Element of X holds x \ (y \ z) = (z \ y) \ (x ) )
proof end;

theorem :: BCIALG_1:67
for X being BCI-algebra holds
( X is p-Semisimple iff for x, y, z being Element of X st y \ x = z \ x holds
y = z )
proof end;

theorem :: BCIALG_1:68
for X being BCI-algebra holds
( X is p-Semisimple iff for x, y, z being Element of X st x \ y = x \ z holds
y = z )
proof end;

theorem :: BCIALG_1:69
for X being non empty BCIStr_0 holds
( X is p-Semisimple BCI-algebra iff for x, y, z being Element of X holds
( (x \ y) \ (x \ z) = z \ y & x \ (0. X) = x ) )
proof end;

theorem :: BCIALG_1:70
for X being non empty BCIStr_0 holds
( X is p-Semisimple BCI-algebra iff ( X is being_I & ( for x, y, z being Element of X holds
( x \ (y \ z) = z \ (y \ x) & x \ (0. X) = x ) ) ) )
proof end;

Lm15: for X being BCI-algebra st ( for x being Element of X holds x  <= x ) holds
for x, y being Element of X holds (x \ y)  = (y \ x)

proof end;

Lm16: for X being BCI-algebra st ( for x, y being Element of X holds (x \ y)  = (y \ x)  ) holds
for x, y being Element of X holds (x ) \ y = (x \ y)

proof end;

Lm17: for X being BCI-algebra st ( for x, y being Element of X holds (x ) \ y = (x \ y)  ) holds
for x, y being Element of X holds (x \ y) \ (y \ x) in BCK-part X

proof end;

Lm18: for X being BCI-algebra st ( for x, y being Element of X holds (x \ y) \ (y \ x) in BCK-part X ) holds
X is quasi-associative

proof end;

Lm19: for X being BCI-algebra holds
( ( for x being Element of X holds x  <= x ) iff for x, y, z being Element of X holds (x \ y) \ z <= x \ (y \ z) )

proof end;

theorem Th71: :: BCIALG_1:71
for X being BCI-algebra holds
( X is quasi-associative iff for x being Element of X holds x  <= x )
proof end;

theorem Th72: :: BCIALG_1:72
for X being BCI-algebra holds
( X is quasi-associative iff for x, y being Element of X holds (x \ y)  = (y \ x)  )
proof end;

theorem Th73: :: BCIALG_1:73
for X being BCI-algebra holds
( X is quasi-associative iff for x, y being Element of X holds (x ) \ y = (x \ y)  )
proof end;

theorem :: BCIALG_1:74
for X being BCI-algebra holds
( X is quasi-associative iff for x, y being Element of X holds (x \ y) \ (y \ x) in BCK-part X )
proof end;

theorem :: BCIALG_1:75
for X being BCI-algebra holds
( X is quasi-associative iff for x, y, z being Element of X holds (x \ y) \ z <= x \ (y \ z) )
proof end;

theorem Th76: :: BCIALG_1:76
for X being BCI-algebra
for x, y being Element of X st X is alternative holds
( x  = x & x \ (x \ y) = y & (x \ y) \ y = x )
proof end;

theorem :: BCIALG_1:77
for X being BCI-algebra
for x, a, b being Element of X st X is alternative & x \ a = x \ b holds
a = b
proof end;

theorem :: BCIALG_1:78
for X being BCI-algebra
for x, a, b being Element of X st X is alternative & a \ x = b \ x holds
a = b
proof end;

theorem :: BCIALG_1:79
for X being BCI-algebra
for x, y being Element of X st X is alternative & x \ y = 0. X holds
x = y
proof end;

theorem :: BCIALG_1:80
for X being BCI-algebra
for x, a, b being Element of X st X is alternative & (x \ a) \ b = 0. X holds
( a = x \ b & b = x \ a )
proof end;

Lm20: for X being BCI-algebra holds
( X is alternative iff X is associative )

proof end;

Lm21: for X being BCI-algebra st X is alternative holds
X is implicative

by Th76;

registration
coherence
for b1 being BCI-algebra st b1 is alternative holds
b1 is associative
by Lm20;
coherence
for b1 being BCI-algebra st b1 is associative holds
b1 is alternative
;
coherence
for b1 being BCI-algebra st b1 is alternative holds
b1 is implicative
by Lm21;
end;

theorem :: BCIALG_1:81
for X being BCI-algebra
for x, y being Element of X st X is alternative holds
(x \ (x \ y)) \ (y \ x) = x
proof end;

theorem :: BCIALG_1:82
for X being BCI-algebra
for x, y being Element of X st X is alternative holds
y \ (y \ (x \ (x \ y))) = y
proof end;

Lm22: for X being BCI-algebra st X is associative holds
X is weakly-positive-implicative

proof end;

Lm23: for X being BCI-algebra st X is p-Semisimple BCI-algebra holds
X is weakly-positive-implicative BCI-algebra

proof end;

registration
coherence
for b1 being BCI-algebra st b1 is associative holds
b1 is weakly-positive-implicative
by Lm22;
coherence
for b1 being BCI-algebra st b1 is p-Semisimple holds
b1 is weakly-positive-implicative
by Lm23;
end;

theorem :: BCIALG_1:83
for X being non empty BCIStr_0 holds
( X is implicative 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 \ x) = y \ (y \ x) ) )
proof end;

theorem Th84: :: BCIALG_1:84
for X being BCI-algebra holds
( X is weakly-positive-implicative iff for x, y being Element of X holds x \ y = ((x \ y) \ y) \ (y ) )
proof end;

Lm24: for X being BCI-algebra
for x, y being Element of X st X is weakly-positive-implicative holds
(x \ (x \ y)) \ (y \ x) = ((y \ (y \ x)) \ (y \ x)) \ (x \ y)

proof end;

Lm25: for X being BCI-algebra holds
( X is positive-implicative iff X is weakly-positive-implicative )

proof end;

registration
coherence
for b1 being BCI-algebra st b1 is positive-implicative holds
b1 is weakly-positive-implicative
by Lm25;
coherence
for b1 being BCI-algebra st b1 is alternative holds
b1 is weakly-positive-implicative
;
end;

theorem :: BCIALG_1:85
for X being BCI-algebra st X is weakly-positive-implicative BCI-algebra holds
for x, y being Element of X holds (x \ (x \ y)) \ (y \ x) = ((y \ (y \ x)) \ (y \ x)) \ (x \ y) by Lm24;

theorem :: BCIALG_1:86
for X being non empty BCIStr_0 holds
( X is positive-implicative 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 \ y = ((x \ y) \ y) \ (y `) & (x \ (x \ y)) \ (y \ x) = ((y \ (y \ x)) \ (y \ x)) \ (x \ y) ) )
proof end;