let X be BCI-algebra; :: thesis: ( AtomSet X is Ideal of X implies for x being Element of BCK-part X
for a being Element of AtomSet X st x \ a in AtomSet X holds
x = 0. X )
set B = BCK-part X;
set P = AtomSet X;
assume A0: AtomSet X is Ideal of X ; :: thesis: for x being Element of BCK-part X
for a being Element of AtomSet X st x \ a in AtomSet X holds
x = 0. X
Lm1: for x being Element of X holds
( x in {(0. X)} iff x in (BCK-part X) /\ (AtomSet X) )

proof

let x be Element of X; :: thesis: ( x in {(0. X)} iff x in (BCK-part X) /\ (AtomSet X) )
thus ( x in {(0. X)} implies x in (BCK-part X) /\ (AtomSet X) ) :: thesis: ( x in (BCK-part X) /\ (AtomSet X) implies x in {(0. X)} )

proof

A1: 0. X in BCK-part X by BCIALG_1:19;
0. X in AtomSet X ;
then 0. X in (BCK-part X) /\ (AtomSet X) by A1, XBOOLE_0:def 4;
hence ( x in {(0. X)} implies x in (BCK-part X) /\ (AtomSet X) ) by TARSKI:def 1; :: thesis: verum

end;

thus ( x in (BCK-part X) /\ (AtomSet X) implies x in {(0. X)} ) :: thesis: verum

proof

assume A1: x in (BCK-part X) /\ (AtomSet X) ; :: thesis: x in {(0. X)}
then A2: x in BCK-part X by XBOOLE_0:def 4;
consider x1 being Element of X such that
B1: ( x = x1 & 0. X <= x1 ) by A2;
C: x in { x2 where x2 is Element of X : x2 is atom } by A1, XBOOLE_0:def 4;
consider x2 being Element of X such that
B2: ( x = x2 & x2 is atom ) by C;
(0. X) \ x = 0. X by B1, BCIALG_1:def 11;
then 0. X = x by B2, BCIALG_1:def 14;
hence x in {(0. X)} by TARSKI:def 1; :: thesis: verum

end;

end;

for x being Element of BCK-part X
for a being Element of AtomSet X st x \ a in AtomSet X holds
x = 0. X

proof

let x be Element of BCK-part X; :: thesis: for a being Element of AtomSet X st x \ a in AtomSet X holds
x = 0. X
let a be Element of AtomSet X; :: thesis: ( x \ a in AtomSet X implies x = 0. X )
assume A1: x \ a in AtomSet X ; :: thesis: x = 0. X
x in AtomSet X by A0, A1, BCIALG_1:def 18;
then x in (BCK-part X) /\ (AtomSet X) by XBOOLE_0:def 4;
then x in {(0. X)} by Lm1;
hence x = 0. X by TARSKI:def 1; :: thesis: verum

end;

hence for x being Element of BCK-part X
for a being Element of AtomSet X st x \ a in AtomSet X holds
x = 0. X ; :: thesis: verum