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

then 0. X in B /\ P by A1, A2, XBOOLE_0:def 4;

then for x being object st x in {(0. X)} holds

x in B /\ P by TARSKI:def 1;

hence {(0. X)} c= B /\ P ; :: thesis: verum

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

( 0. X in BCK-part X & 0. X in p-Semisimple-part X )
by BCIALG_1:19;
let x be object ; :: 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;

ex x2 being Element of X st

( x = x2 & x2 is minimal ) by A2, A4;

then x = 0. X by A7;

hence x in {(0. X)} by TARSKI:def 1; :: thesis: verum

end;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;

ex x2 being Element of X st

( x = x2 & x2 is minimal ) by A2, A4;

then x = 0. X by A7;

hence x in {(0. X)} by TARSKI:def 1; :: thesis: verum

then 0. X in B /\ P by A1, A2, XBOOLE_0:def 4;

then for x being object st x in {(0. X)} holds

x in B /\ P by TARSKI:def 1;

hence {(0. X)} c= B /\ P ; :: thesis: verum