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 (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) )
( 0. X in BCK-part X & 0. X in AtomSet X ) by BCIALG_1:19;
then 0. X in (BCK-part X) /\ (AtomSet X) by XBOOLE_0:def 4;
hence ( x in {(0. X)} implies x in (BCK-part X) /\ (AtomSet X) ) by TARSKI:def 1; :: thesis: ( x in (BCK-part X) /\ (AtomSet X) implies x in {(0. X)} )
thus ( x in (BCK-part X) /\ (AtomSet X) implies x in {(0. X)} ) :: thesis: verum

proof

assume A2: x in (BCK-part X) /\ (AtomSet X) ; :: 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 A2, XBOOLE_0:def 4;
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 A4, BCIALG_1:def 18;
then x in (BCK-part X) /\ (AtomSet X) 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