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 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;
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 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
proof
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;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in {(0. X)} or x in 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;