let X be non empty BCIStr_0 ; :: thesis: ( 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 ) )
thus ( X is p-Semisimple BCI-algebra implies for x, y, z being Element of X holds
( (x \ y) \ (x \ z) = z \ y & x \ (0. X) = x ) ) by Th2, Th56; :: thesis: ( ( for x, y, z being Element of X holds
( (x \ y) \ (x \ z) = z \ y & x \ (0. X) = x ) ) implies X is p-Semisimple BCI-algebra )
assume A1: for x, y, z being Element of X holds
( (x \ y) \ (x \ z) = z \ y & x \ (0. X) = x ) ; :: thesis: X is p-Semisimple BCI-algebra
A2: X is being_I

proof

now

let x be Element of X; :: thesis: x \ x = 0. X
x \ x = (x \ (0. X)) \ x by A1
.= (x \ (0. X)) \ (x \ (0. X)) by A1
.= (0. X) ` by A1 ;
hence x \ x = 0. X by A1; :: thesis: verum

end;

hence X is being_I by Def5; :: thesis: verum

end;

A3: X is being_BCI-4

proof

now

let x, y be Element of X; :: thesis: ( x \ y = 0. X & y \ x = 0. X implies x = y )
assume A4: ( x \ y = 0. X & y \ x = 0. X ) ; :: thesis: x = y
x = x \ (0. X) by A1
.= (x \ (0. X)) \ (x \ y) by A1, A4
.= y \ (0. X) by A1 ;
hence x = y by A1; :: thesis: verum

end;

hence X is being_BCI-4 by Def7; :: thesis: verum

end;

now

let x, y, z be Element of X; :: 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 ) )
thus ((x \ y) \ (x \ z)) \ (z \ y) = 0. X :: thesis: ( (x \ (x \ y)) \ y = 0. X & ( for x, y being Element of X holds x \ (x \ y) = y ) )

proof

((x \ y) \ (x \ z)) \ (z \ y) = (z \ y) \ (z \ y) by A1
.= ((z \ y) \ (0. X)) \ (z \ y) by A1
.= ((z \ y) \ (0. X)) \ ((z \ y) \ (0. X)) by A1
.= (0. X) ` by A1 ;
hence ((x \ y) \ (x \ z)) \ (z \ y) = 0. X by A1; :: thesis: verum

end;

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

proof

(x \ (x \ y)) \ y = ((x \ (0. X)) \ (x \ y)) \ y by A1
.= (y \ (0. X)) \ y by A1
.= (y \ (0. X)) \ (y \ (0. X)) by A1
.= (0. X) ` by A1 ;
hence (x \ (x \ y)) \ y = 0. X by A1; :: thesis: verum

end;

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

proof

let x, y be Element of X; :: thesis: x \ (x \ y) = y
x \ (x \ y) = (x \ (0. X)) \ (x \ y) by A1;
then x \ (x \ y) = y \ (0. X) by A1;
hence x \ (x \ y) = y by A1; :: thesis: verum

end;

end;

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