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 that
A1: B = BCK-part X and
A2: 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 A3: x in B /\ P ; :: thesis: x in {(0. X)}
then A4: x in P by XBOOLE_0:def 4;
A5: x in B by A3, XBOOLE_0:def 4;
then A6: ex x1 being Element of X st
( x = x1 & 0. X <= x1 ) by A1;
reconsider x = x as Element of X by A1, A5;
A7: (0. X) \ x = 0. X by A6, BCIALG_1:def 11;
ex x2 being Element of X st
( x = x2 & x2 is minimal ) by A2, A4;
then x = 0. X by A7, BCIALG_1:def 14;
hence x in {(0. X)} by TARSKI:def 1; :: thesis: verum

end;

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