let X be BCI-algebra; :: thesis: ( X is p-Semisimple implies BCK-part X = {(0. X)} )

assume A1: X is p-Semisimple ; :: thesis: BCK-part X = {(0. X)}

thus BCK-part X c= {(0. X)} :: according to XBOOLE_0:def 10 :: thesis: {(0. X)} c= BCK-part X

assume A1: X is p-Semisimple ; :: thesis: BCK-part X = {(0. X)}

thus BCK-part X c= {(0. X)} :: according to XBOOLE_0:def 10 :: thesis: {(0. X)} c= BCK-part X

proof

thus
{(0. X)} c= BCK-part X
:: thesis: verum
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in BCK-part X or x in {(0. X)} )

assume A2: x in BCK-part X ; :: thesis: x in {(0. X)}

then A3: ex x1 being Element of X st

( x = x1 & 0. X <= x1 ) ;

reconsider x = x as Element of X by A2;

(x `) ` = x by A1;

then (0. X) ` = x by A3;

then x = 0. X by Def5;

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

end;assume A2: x in BCK-part X ; :: thesis: x in {(0. X)}

then A3: ex x1 being Element of X st

( x = x1 & 0. X <= x1 ) ;

reconsider x = x as Element of X by A2;

(x `) ` = x by A1;

then (0. X) ` = x by A3;

then x = 0. X by Def5;

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

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in {(0. X)} or x in BCK-part X )

assume A4: x in {(0. X)} ; :: thesis: x in BCK-part X

then reconsider x = x as Element of X by TARSKI:def 1;

x = 0. X by A4, TARSKI:def 1;

then x ` = 0. X by Def5;

then 0. X <= x ;

hence x in BCK-part X ; :: thesis: verum

end;assume A4: x in {(0. X)} ; :: thesis: x in BCK-part X

then reconsider x = x as Element of X by TARSKI:def 1;

x = 0. X by A4, TARSKI:def 1;

then x ` = 0. X by Def5;

then 0. X <= x ;

hence x in BCK-part X ; :: thesis: verum