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) )

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

for a being Element of AtomSet X st x \ a in AtomSet X holds

x = 0. X ; :: thesis: verum

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

assume A4:
AtomSet X is Ideal of X
; :: thesis: for x being Element of BCK-part X
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

end;( 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;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

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

hence
for x being Element of BCK-part X
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;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

for a being Element of AtomSet X st x \ a in AtomSet X holds

x = 0. X ; :: thesis: verum