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

proof

assume B1: 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
C: (x \ y) \ x = (x \ x) \ y by BCIALG_1:7
.= y ` by BCIALG_1:def 5
.= 0. X by BCIALG_1:def 8 ;
C1: (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 ;
x \ (x \ y) <= x by C1, BCIALG_1:def 11;
then A1: x \ (x \ y) in A by P141;
(x \ (x \ y)) \ y = 0. X by BCIALG_1:1;
then x \ (x \ y) <= y by BCIALG_1:def 11;
then x \ (x \ y) in I by P141;
then x \ (x \ y) in {(0. X)} by B1, A1, XBOOLE_0:def 4;
then x \ (x \ y) = 0. X by TARSKI:def 1;
hence x \ y = x by C, BCIALG_1:def 7; :: thesis: verum

end;

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

proof

assume A1: 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

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in A /\ I or x in {(0. X)} )
assume C: 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 C, XBOOLE_0:def 4;
xxx \ xx = xxx by A1;
then x = 0. X by BCIALG_1:def 5;
hence x in {(0. X)} by TARSKI:def 1; :: thesis: verum

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in {(0. X)} or x in A /\ I )
assume A0: x in {(0. X)} ; :: thesis: x in A /\ I
A2: x = 0. X by A0, TARSKI:def 1;
A3: 0. X in A by BCIALG_1:def 18;
0. X in I by BCIALG_1:def 18;
hence x in A /\ I by A2, A3, XBOOLE_0:def 4; :: thesis: verum

end;