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 )

for x being Element of X holds (0. X) \ x = 0. X

hence X is BCK-algebra by BCIALG_1:def 8; :: thesis: verum

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 A5:
P = {(0. X)}
; :: thesis: X is BCK-algebra
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

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;thus P c= {(0. X)} :: according to XBOOLE_0:def 10 :: thesis: {(0. X)} c= P

proof

0. X in P
by A1;
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;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

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

for x being Element of X holds (0. X) \ x = 0. X

proof

then
for x being Element of X holds x ` = 0. X
;
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;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

hence X is BCK-algebra by BCIALG_1:def 8; :: thesis: verum