let X be BCK-algebra; :: thesis: for A, I being Ideal of X holds

( A /\ I = {(0. X)} iff for x being Element of A

for y being Element of I holds x \ y = x )

let A, I be Ideal of X; :: thesis: ( A /\ I = {(0. X)} iff for x being Element of A

for y being Element of I holds x \ y = x )

thus ( A /\ I = {(0. X)} implies for x being Element of A

for y being Element of I holds x \ y = x ) :: thesis: ( ( for x being Element of A

for y being Element of I holds x \ y = x ) implies A /\ I = {(0. X)} )

for y being Element of I holds x \ y = x ) implies A /\ I = {(0. X)} ) :: thesis: verum

( A /\ I = {(0. X)} iff for x being Element of A

for y being Element of I holds x \ y = x )

let A, I be Ideal of X; :: thesis: ( A /\ I = {(0. X)} iff for x being Element of A

for y being Element of I holds x \ y = x )

thus ( A /\ I = {(0. X)} implies for x being Element of A

for y being Element of I holds x \ y = x ) :: thesis: ( ( for x being Element of A

for y being Element of I holds x \ y = x ) implies A /\ I = {(0. X)} )

proof

thus
( ( for x being Element of A
assume A1:
A /\ I = {(0. X)}
; :: thesis: for x being Element of A

for y being Element of I holds x \ y = x

let x be Element of A; :: thesis: for y being Element of I holds x \ y = x

let y be Element of I; :: thesis: x \ y = x

(x \ (x \ y)) \ y = 0. X by BCIALG_1:1;

then x \ (x \ y) <= y ;

then A2: x \ (x \ y) in I by Th5;

(x \ (x \ y)) \ x = (x \ x) \ (x \ y) by BCIALG_1:7

.= (x \ y) ` by BCIALG_1:def 5

.= 0. X by BCIALG_1:def 8 ;

then x \ (x \ y) <= x ;

then x \ (x \ y) in A by Th5;

then x \ (x \ y) in {(0. X)} by A1, A2, XBOOLE_0:def 4;

then A3: x \ (x \ y) = 0. X by TARSKI:def 1;

(x \ y) \ x = (x \ x) \ y by BCIALG_1:7

.= y ` by BCIALG_1:def 5

.= 0. X by BCIALG_1:def 8 ;

hence x \ y = x by A3, BCIALG_1:def 7; :: thesis: verum

end;for y being Element of I holds x \ y = x

let x be Element of A; :: thesis: for y being Element of I holds x \ y = x

let y be Element of I; :: thesis: x \ y = x

(x \ (x \ y)) \ y = 0. X by BCIALG_1:1;

then x \ (x \ y) <= y ;

then A2: x \ (x \ y) in I by Th5;

(x \ (x \ y)) \ x = (x \ x) \ (x \ y) by BCIALG_1:7

.= (x \ y) ` by BCIALG_1:def 5

.= 0. X by BCIALG_1:def 8 ;

then x \ (x \ y) <= x ;

then x \ (x \ y) in A by Th5;

then x \ (x \ y) in {(0. X)} by A1, A2, XBOOLE_0:def 4;

then A3: x \ (x \ y) = 0. X by TARSKI:def 1;

(x \ y) \ x = (x \ x) \ y by BCIALG_1:7

.= y ` by BCIALG_1:def 5

.= 0. X by BCIALG_1:def 8 ;

hence x \ y = x by A3, BCIALG_1:def 7; :: thesis: verum

for y being Element of I holds x \ y = x ) implies A /\ I = {(0. X)} ) :: thesis: verum

proof

assume A4:
for x being Element of A

for y being Element of I holds x \ y = x ; :: thesis: A /\ I = {(0. X)}

thus A /\ I c= {(0. X)} :: according to XBOOLE_0:def 10 :: thesis: {(0. X)} c= A /\ I

assume x in {(0. X)} ; :: thesis: x in A /\ I

then A6: x = 0. X by TARSKI:def 1;

( 0. X in A & 0. X in I ) by BCIALG_1:def 18;

hence x in A /\ I by A6, XBOOLE_0:def 4; :: thesis: verum

end;for y being Element of I holds x \ y = x ; :: thesis: A /\ I = {(0. X)}

thus A /\ I c= {(0. X)} :: according to XBOOLE_0:def 10 :: thesis: {(0. X)} c= A /\ I

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in {(0. X)} or x in A /\ I )
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in A /\ I or x in {(0. X)} )

assume A5: x in A /\ I ; :: thesis: x in {(0. X)}

then reconsider xxx = x as Element of A by XBOOLE_0:def 4;

reconsider xx = x as Element of I by A5, XBOOLE_0:def 4;

xxx \ xx = xxx by A4;

then x = 0. X by BCIALG_1:def 5;

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

end;assume A5: x in A /\ I ; :: thesis: x in {(0. X)}

then reconsider xxx = x as Element of A by XBOOLE_0:def 4;

reconsider xx = x as Element of I by A5, XBOOLE_0:def 4;

xxx \ xx = xxx by A4;

then x = 0. X by BCIALG_1:def 5;

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

assume x in {(0. X)} ; :: thesis: x in A /\ I

then A6: x = 0. X by TARSKI:def 1;

( 0. X in A & 0. X in I ) by BCIALG_1:def 18;

hence x in A /\ I by A6, XBOOLE_0:def 4; :: thesis: verum