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

( I is positive-implicative-ideal of X iff for x, y being Element of X st (x \ y) \ y in I holds

x \ y in I )

let I be Ideal of X; :: thesis: ( I is positive-implicative-ideal of X iff for x, y being Element of X st (x \ y) \ y in I holds

x \ y in I )

thus ( I is positive-implicative-ideal of X implies for x, y being Element of X st (x \ y) \ y in I holds

x \ y in I ) :: thesis: ( ( for x, y being Element of X st (x \ y) \ y in I holds

x \ y in I ) implies I is positive-implicative-ideal of X )

x \ y in I ) implies I is positive-implicative-ideal of X ) :: thesis: verum

( I is positive-implicative-ideal of X iff for x, y being Element of X st (x \ y) \ y in I holds

x \ y in I )

let I be Ideal of X; :: thesis: ( I is positive-implicative-ideal of X iff for x, y being Element of X st (x \ y) \ y in I holds

x \ y in I )

thus ( I is positive-implicative-ideal of X implies for x, y being Element of X st (x \ y) \ y in I holds

x \ y in I ) :: thesis: ( ( for x, y being Element of X st (x \ y) \ y in I holds

x \ y in I ) implies I is positive-implicative-ideal of X )

proof

thus
( ( for x, y being Element of X st (x \ y) \ y in I holds
assume A1:
I is positive-implicative-ideal of X
; :: thesis: for x, y being Element of X st (x \ y) \ y in I holds

x \ y in I

let x, y be Element of X; :: thesis: ( (x \ y) \ y in I implies x \ y in I )

y \ y = 0. X by BCIALG_1:def 5;

then A2: y \ y in I by A1, Def8;

assume (x \ y) \ y in I ; :: thesis: x \ y in I

hence x \ y in I by A1, A2, Def8; :: thesis: verum

end;x \ y in I

let x, y be Element of X; :: thesis: ( (x \ y) \ y in I implies x \ y in I )

y \ y = 0. X by BCIALG_1:def 5;

then A2: y \ y in I by A1, Def8;

assume (x \ y) \ y in I ; :: thesis: x \ y in I

hence x \ y in I by A1, A2, Def8; :: thesis: verum

x \ y in I ) implies I is positive-implicative-ideal of X ) :: thesis: verum

proof

assume A3:
for x, y being Element of X st (x \ y) \ y in I holds

x \ y in I ; :: thesis: I is positive-implicative-ideal of X

A4: for x, y, z being Element of X st (x \ y) \ z in I & y \ z in I holds

x \ z in I

hence I is positive-implicative-ideal of X by A4, Def8; :: thesis: verum

end;x \ y in I ; :: thesis: I is positive-implicative-ideal of X

A4: for x, y, z being Element of X st (x \ y) \ z in I & y \ z in I holds

x \ z in I

proof

0. X in I
by BCIALG_1:def 18;
let x, y, z be Element of X; :: thesis: ( (x \ y) \ z in I & y \ z in I implies x \ z in I )

assume that

A5: (x \ y) \ z in I and

A6: y \ z in I ; :: thesis: x \ z in I

(((x \ z) \ z) \ ((x \ y) \ z)) \ ((x \ z) \ (x \ y)) = 0. X by BCIALG_1:def 3;

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

then (((x \ z) \ z) \ ((x \ y) \ z)) \ (y \ z) <= ((x \ z) \ (x \ y)) \ (y \ z) by BCIALG_1:5;

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

then ((((x \ z) \ z) \ ((x \ y) \ z)) \ (y \ z)) \ (0. X) = 0. X ;

then (((x \ z) \ z) \ ((x \ y) \ z)) \ (y \ z) = 0. X by BCIALG_1:2;

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

then ((x \ z) \ z) \ ((x \ y) \ z) in I by A6, Th5;

then (x \ z) \ z in I by A5, BCIALG_1:def 18;

hence x \ z in I by A3; :: thesis: verum

end;assume that

A5: (x \ y) \ z in I and

A6: y \ z in I ; :: thesis: x \ z in I

(((x \ z) \ z) \ ((x \ y) \ z)) \ ((x \ z) \ (x \ y)) = 0. X by BCIALG_1:def 3;

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

then (((x \ z) \ z) \ ((x \ y) \ z)) \ (y \ z) <= ((x \ z) \ (x \ y)) \ (y \ z) by BCIALG_1:5;

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

then ((((x \ z) \ z) \ ((x \ y) \ z)) \ (y \ z)) \ (0. X) = 0. X ;

then (((x \ z) \ z) \ ((x \ y) \ z)) \ (y \ z) = 0. X by BCIALG_1:2;

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

then ((x \ z) \ z) \ ((x \ y) \ z) in I by A6, Th5;

then (x \ z) \ z in I by A5, BCIALG_1:def 18;

hence x \ z in I by A3; :: thesis: verum

hence I is positive-implicative-ideal of X by A4, Def8; :: thesis: verum