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

proof

assume A2: X is BCK-algebra ; :: thesis: P = {(0. X)}
thus P c= {(0. X)} :: according to XBOOLE_0:def 10 :: thesis: {(0. X)} c= P

proof

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

end;

0. X in P by A1;
then for x being object st x in {(0. X)} holds
x in P by TARSKI:def 1;
hence {(0. X)} c= P ; :: thesis: verum

end;

assume A5: P = {(0. X)} ; :: thesis: X is BCK-algebra
for x being Element of X holds (0. X) \ x = 0. X

proof

let x be Element of X; :: thesis: (0. X) \ x = 0. X
0. X in P by A5, TARSKI:def 1;
then (0. X) \ x in P by A1, BCIALG_1:33;
hence (0. X) \ x = 0. X by A5, TARSKI:def 1; :: thesis: verum

end;

then for x being Element of X holds x ` = 0. X ;
hence X is BCK-algebra by BCIALG_1:def 8; :: thesis: verum