let X be BCI-algebra; :: thesis: for B, P being non empty Subset of X
for X being BCI-algebra st B = BCK-part X & P = p-Semisimple-part X holds
B /\ P = {(0. X)}
let B, P be non empty Subset of X; :: thesis: for X being BCI-algebra st B = BCK-part X & P = p-Semisimple-part X holds
B /\ P = {(0. X)}
let X be BCI-algebra; :: thesis: ( B = BCK-part X & P = p-Semisimple-part X implies B /\ P = {(0. X)} )
assume A1: ( B = BCK-part X & P = p-Semisimple-part X ) ; :: thesis: B /\ P = {(0. X)}
thus B /\ P c= {(0. X)} :: according to XBOOLE_0:def 10 :: thesis: {(0. X)} c= B /\ P

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in B /\ P or x in {(0. X)} )
assume x in B /\ P ; :: thesis: x in {(0. X)}
then B1: ( x in B & x in P ) by XBOOLE_0:def 4;
consider x1 being Element of X such that
B2: ( x = x1 & 0. X <= x1 ) by A1, B1;
reconsider x = x as Element of X by B2;
B2a: (0. X) \ x = 0. X by B2, BCIALG_1:def 11;
consider x2 being Element of X such that
B3: ( x = x2 & x2 is minimal ) by A1, B1;
x = 0. X by B3, B2a, BCIALG_1:def 14;
hence x in {(0. X)} by TARSKI:def 1; :: thesis: verum

end;

A2: 0. X in BCK-part X by BCIALG_1:19;
0. X in p-Semisimple-part X ;
then A3: 0. X in B /\ P by A1, A2, XBOOLE_0:def 4;
for x being set st x in {(0. X)} holds
x in B /\ P by A3, TARSKI:def 1;
hence {(0. X)} c= B /\ P by TARSKI:def 3; :: thesis: verum