let X be BCI-algebra; :: thesis: for B being non empty Subset of X
for X being BCI-algebra st B = BCK-part X holds
( X is p-Semisimple BCI-algebra iff B = {(0. X)} )
let B be non empty Subset of X; :: thesis: for X being BCI-algebra st B = BCK-part X holds
( X is p-Semisimple BCI-algebra iff B = {(0. X)} )
let X be BCI-algebra; :: thesis: ( B = BCK-part X implies ( X is p-Semisimple BCI-algebra iff B = {(0. X)} ) )
assume A1: B = BCK-part X ; :: thesis: ( X is p-Semisimple BCI-algebra iff B = {(0. X)} )
thus ( X is p-Semisimple BCI-algebra implies B = {(0. X)} ) :: thesis: ( B = {(0. X)} implies X is p-Semisimple BCI-algebra )

proof

assume A2: X is p-Semisimple BCI-algebra ; :: thesis: B = {(0. X)}
thus B c= {(0. X)} :: according to XBOOLE_0:def 10 :: thesis: {(0. X)} c= B

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in B or x in {(0. X)} )
assume A3: x in B ; :: thesis: x in {(0. X)}
then A4: ex x1 being Element of X st
( x = x1 & 0. X <= x1 ) by A1;
reconsider x = x as Element of X by A1, A3;
(x `) ` = x by A2, BCIALG_1:def 26;
then (0. X) ` = x by A4;
then x = 0. X by BCIALG_1:def 5;
hence x in {(0. X)} by TARSKI:def 1; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in {(0. X)} or x in B )
assume A5: x in {(0. X)} ; :: thesis: x in B
then reconsider x = x as Element of X by TARSKI:def 1;
x = 0. X by A5, TARSKI:def 1;
then x ` = 0. X by BCIALG_1:def 5;
then 0. X <= x ;
hence x in B by A1; :: thesis: verum

end;

assume A6: B = {(0. X)} ; :: thesis: X is p-Semisimple BCI-algebra
for x being Element of X holds (x `) ` = x

proof

let x be Element of X; :: thesis: (x `) ` = x
(0. X) \ (x \ ((0. X) \ ((0. X) \ x))) = ((0. X),(x \ ((0. X) \ ((0. X) \ x)))) to_power 1 by BCIALG_2:2
.= (((0. X),x) to_power 1) \ (((0. X),((0. X) \ ((0. X) \ x))) to_power 1) by BCIALG_2:18
.= (((0. X),x) to_power 1) \ (((0. X),x) to_power 1) by BCIALG_2:8
.= 0. X by BCIALG_1:def 5 ;
then 0. X <= x \ ((0. X) \ ((0. X) \ x)) ;
then x \ ((0. X) \ ((0. X) \ x)) in B by A1;
then A7: x \ ((0. X) \ ((0. X) \ x)) = 0. X by A6, TARSKI:def 1;
((0. X) \ ((0. X) \ x)) \ x = ((0. X) \ x) \ ((0. X) \ x) by BCIALG_1:7
.= 0. X by BCIALG_1:def 5 ;
hence (x `) ` = x by A7, BCIALG_1:def 7; :: thesis: verum

end;

hence X is p-Semisimple BCI-algebra by BCIALG_1:54; :: thesis: verum