let X be non empty BCIStr_0 ; :: thesis: ( 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 ) ) ) )

thus ( X is p-Semisimple BCI-algebra implies ( X is being_I & ( for x, y, z being Element of X holds

( x \ (y \ z) = z \ (y \ x) & x \ (0. X) = x ) ) ) ) by Th2, Th57; :: thesis: ( X is being_I & ( for x, y, z being Element of X holds

( x \ (y \ z) = z \ (y \ x) & x \ (0. X) = x ) ) implies X is p-Semisimple BCI-algebra )

assume that

A1: X is being_I and

A2: for x, y, z being Element of X holds

( x \ (y \ z) = z \ (y \ x) & x \ (0. X) = x ) ; :: thesis: X is p-Semisimple BCI-algebra

hence X is p-Semisimple BCI-algebra by A1, A3, Def26, Th1; :: thesis: verum

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

thus ( X is p-Semisimple BCI-algebra implies ( X is being_I & ( for x, y, z being Element of X holds

( x \ (y \ z) = z \ (y \ x) & x \ (0. X) = x ) ) ) ) by Th2, Th57; :: thesis: ( X is being_I & ( for x, y, z being Element of X holds

( x \ (y \ z) = z \ (y \ x) & x \ (0. X) = x ) ) implies X is p-Semisimple BCI-algebra )

assume that

A1: X is being_I and

A2: for x, y, z being Element of X holds

( x \ (y \ z) = z \ (y \ x) & x \ (0. X) = x ) ; :: thesis: X is p-Semisimple BCI-algebra

A3: now :: thesis: for x, y, z being Element of X holds

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

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

let x, y, z be Element of X; :: thesis: ( x \ x = 0. X & ((x \ y) \ (x \ z)) \ (z \ y) = 0. X & (x \ (x \ y)) \ y = 0. X & ( for x, y being Element of X holds x \ (x \ y) = y ) )

thus x \ x = 0. X by A1; :: thesis: ( ((x \ y) \ (x \ z)) \ (z \ y) = 0. X & (x \ (x \ y)) \ y = 0. X & ( for x, y being Element of X holds x \ (x \ y) = y ) )

((x \ y) \ (x \ z)) \ (z \ y) = (z \ (x \ (x \ y))) \ (z \ y) by A2

.= (z \ (y \ (x \ x))) \ (z \ y) by A2

.= (z \ (y \ (0. X))) \ (z \ y) by A1

.= (z \ y) \ (z \ y) by A2 ;

hence ((x \ y) \ (x \ z)) \ (z \ y) = 0. X by A1; :: thesis: ( (x \ (x \ y)) \ y = 0. X & ( for x, y being Element of X holds x \ (x \ y) = y ) )

(x \ (x \ y)) \ y = (y \ (x \ x)) \ y by A2

.= (y \ (0. X)) \ y by A1

.= y \ y by A2 ;

hence (x \ (x \ y)) \ y = 0. X by A1; :: thesis: for x, y being Element of X holds x \ (x \ y) = y

thus for x, y being Element of X holds x \ (x \ y) = y :: thesis: verum

end;thus x \ x = 0. X by A1; :: thesis: ( ((x \ y) \ (x \ z)) \ (z \ y) = 0. X & (x \ (x \ y)) \ y = 0. X & ( for x, y being Element of X holds x \ (x \ y) = y ) )

((x \ y) \ (x \ z)) \ (z \ y) = (z \ (x \ (x \ y))) \ (z \ y) by A2

.= (z \ (y \ (x \ x))) \ (z \ y) by A2

.= (z \ (y \ (0. X))) \ (z \ y) by A1

.= (z \ y) \ (z \ y) by A2 ;

hence ((x \ y) \ (x \ z)) \ (z \ y) = 0. X by A1; :: thesis: ( (x \ (x \ y)) \ y = 0. X & ( for x, y being Element of X holds x \ (x \ y) = y ) )

(x \ (x \ y)) \ y = (y \ (x \ x)) \ y by A2

.= (y \ (0. X)) \ y by A1

.= y \ y by A2 ;

hence (x \ (x \ y)) \ y = 0. X by A1; :: thesis: for x, y being Element of X holds x \ (x \ y) = y

thus for x, y being Element of X holds x \ (x \ y) = y :: thesis: verum

now :: thesis: for x, y being Element of X st x \ y = 0. X & y \ x = 0. X holds

x = y

then
X is being_BCI-4
;x = y

let x, y be Element of X; :: thesis: ( x \ y = 0. X & y \ x = 0. X implies x = y )

assume that

A4: x \ y = 0. X and

y \ x = 0. X ; :: thesis: x = y

x = x \ (0. X) by A2

.= y \ (x \ x) by A2, A4

.= y \ (0. X) by A1 ;

hence x = y by A2; :: thesis: verum

end;assume that

A4: x \ y = 0. X and

y \ x = 0. X ; :: thesis: x = y

x = x \ (0. X) by A2

.= y \ (x \ x) by A2, A4

.= y \ (0. X) by A1 ;

hence x = y by A2; :: thesis: verum

hence X is p-Semisimple BCI-algebra by A1, A3, Def26, Th1; :: thesis: verum