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;
A1: for x being Element of X holds
( x in {(0. X)} iff x in () /\ () )
proof
let x be Element of X; :: thesis: ( x in {(0. X)} iff x in () /\ () )
( 0. X in BCK-part X & 0. X in AtomSet X ) by BCIALG_1:19;
then 0. X in () /\ () by XBOOLE_0:def 4;
hence ( x in {(0. X)} implies x in () /\ () ) by TARSKI:def 1; :: thesis: ( x in () /\ () implies x in {(0. X)} )
thus ( x in () /\ () implies x in {(0. X)} ) :: thesis: verum
proof
assume A2: x in () /\ () ; :: thesis: x in {(0. X)}
then x in BCK-part X by XBOOLE_0:def 4;
then ex x1 being Element of X st
( x = x1 & 0. X <= x1 ) ;
then A3: (0. X) \ x = 0. X ;
x in { x2 where x2 is Element of X : x2 is minimal } by ;
then ex x2 being Element of X st
( x = x2 & x2 is minimal ) ;
then 0. X = x by A3;
hence x in {(0. X)} by TARSKI:def 1; :: thesis: verum
end;
end;
assume A4: 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

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 x \ a in AtomSet X ; :: thesis: x = 0. X
then x in AtomSet X by ;
then x in () /\ () by XBOOLE_0:def 4;
then x in {(0. X)} by A1;
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