let X be BCI-algebra; :: thesis: ( X is p-Semisimple implies BCK-part X = {(0. X)} )
assume A1: X is p-Semisimple ; :: thesis: BCK-part X = {(0. X)}
thus BCK-part X c= {(0. X)} :: according to XBOOLE_0:def 10 :: thesis: {(0. X)} c= BCK-part X

proof

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

end;

thus {(0. X)} c= BCK-part X :: thesis: verum

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in {(0. X)} or x in BCK-part X )
assume A4: x in {(0. X)} ; :: thesis: x in BCK-part X
then reconsider x = x as Element of X by TARSKI:def 1;
x = 0. X by A4, TARSKI:def 1;
then x ` = 0. X by Def5;
then 0. X <= x ;
hence x in BCK-part X ; :: thesis: verum

end;