let X be BCI-algebra; :: thesis: ( X is BCK-positive-implicative BCK-algebra iff X is BCK-algebra of 0 ,1, 0 ,1 )

thus ( X is BCK-positive-implicative BCK-algebra implies X is BCK-algebra of 0 ,1, 0 ,1 ) :: thesis: ( X is BCK-algebra of 0 ,1, 0 ,1 implies X is BCK-positive-implicative BCK-algebra )

for x, y being Element of X holds x \ y = (x \ y) \ y

thus ( X is BCK-positive-implicative BCK-algebra implies X is BCK-algebra of 0 ,1, 0 ,1 ) :: thesis: ( X is BCK-algebra of 0 ,1, 0 ,1 implies X is BCK-positive-implicative BCK-algebra )

proof

assume A6:
X is BCK-algebra of 0 ,1, 0 ,1
; :: thesis: X is BCK-positive-implicative BCK-algebra
assume A1:
X is BCK-positive-implicative BCK-algebra
; :: thesis: X is BCK-algebra of 0 ,1, 0 ,1

for x, y being Element of X holds Polynom (0,1,x,y) = Polynom (0,1,y,x)

end;for x, y being Element of X holds Polynom (0,1,x,y) = Polynom (0,1,y,x)

proof

hence
X is BCK-algebra of 0 ,1, 0 ,1
by A1, Def3; :: thesis: verum
let x, y be Element of X; :: thesis: Polynom (0,1,x,y) = Polynom (0,1,y,x)

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

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

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

x \ (x \ y) = (x \ (x \ y)) \ (x \ y) by A1, BCIALG_3:28;

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

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

then A3: (x \ (x \ y)) \ (y \ x) <= (y \ (y \ x)) \ (x \ y) by BCIALG_1:7;

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

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

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

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

y \ (y \ x) = (y \ (y \ x)) \ (y \ x) by A1, BCIALG_3:28;

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

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

then A5: (x \ (x \ y)) \ (y \ x) = (y \ (y \ x)) \ (x \ y) by A3, Th2;

(((x,(x \ y)) to_power 1),(y \ x)) to_power 1 = ((x,(x \ y)) to_power 1) \ (y \ x) by BCIALG_2:2

.= (x \ (x \ y)) \ (y \ x) by BCIALG_2:2

.= ((y \ (y \ x)),(x \ y)) to_power 1 by A5, BCIALG_2:2

.= (((y,(y \ x)) to_power 1),(x \ y)) to_power 1 by BCIALG_2:2 ;

hence Polynom (0,1,x,y) = Polynom (0,1,y,x) ; :: thesis: verum

end;(x \ y) \ (x \ y) = 0. X by BCIALG_1:def 5;

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

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

x \ (x \ y) = (x \ (x \ y)) \ (x \ y) by A1, BCIALG_3:28;

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

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

then A3: (x \ (x \ y)) \ (y \ x) <= (y \ (y \ x)) \ (x \ y) by BCIALG_1:7;

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

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

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

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

y \ (y \ x) = (y \ (y \ x)) \ (y \ x) by A1, BCIALG_3:28;

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

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

then A5: (x \ (x \ y)) \ (y \ x) = (y \ (y \ x)) \ (x \ y) by A3, Th2;

(((x,(x \ y)) to_power 1),(y \ x)) to_power 1 = ((x,(x \ y)) to_power 1) \ (y \ x) by BCIALG_2:2

.= (x \ (x \ y)) \ (y \ x) by BCIALG_2:2

.= ((y \ (y \ x)),(x \ y)) to_power 1 by A5, BCIALG_2:2

.= (((y,(y \ x)) to_power 1),(x \ y)) to_power 1 by BCIALG_2:2 ;

hence Polynom (0,1,x,y) = Polynom (0,1,y,x) ; :: thesis: verum

for x, y being Element of X holds x \ y = (x \ y) \ y

proof

hence
X is BCK-positive-implicative BCK-algebra
by A6, BCIALG_3:28; :: thesis: verum
let x, y be Element of X; :: thesis: x \ y = (x \ y) \ y

A7: Polynom (0,1,x,(x \ y)) = Polynom (0,1,(x \ y),x) by A6, Def3;

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

.= y ` by BCIALG_1:def 5

.= 0. X by A6, BCIALG_1:def 8 ;

then A9: ((x \ y) \ ((x \ y) \ x)) \ (x \ (x \ y)) = (x \ y) \ (x \ (x \ y)) by BCIALG_1:2

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

.= (x \ y) \ y by BCIALG_1:8 ;

A10: (x \ (x \ (x \ y))) \ ((x \ y) \ x) = (x \ y) \ ((x \ y) \ x) by BCIALG_1:8

.= x \ y by A8, BCIALG_1:2 ;

(x \ (x \ (x \ y))) \ ((x \ y) \ x) = ((x,(x \ (x \ y))) to_power 1) \ ((x \ y) \ x) by BCIALG_2:2

.= ((((x \ y),((x \ y) \ x)) to_power 1),(x \ (x \ y))) to_power 1 by A7, BCIALG_2:2

.= (((x \ y) \ ((x \ y) \ x)),(x \ (x \ y))) to_power 1 by BCIALG_2:2

.= ((x \ y) \ ((x \ y) \ x)) \ (x \ (x \ y)) by BCIALG_2:2 ;

hence x \ y = (x \ y) \ y by A10, A9; :: thesis: verum

end;A7: Polynom (0,1,x,(x \ y)) = Polynom (0,1,(x \ y),x) by A6, Def3;

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

.= y ` by BCIALG_1:def 5

.= 0. X by A6, BCIALG_1:def 8 ;

then A9: ((x \ y) \ ((x \ y) \ x)) \ (x \ (x \ y)) = (x \ y) \ (x \ (x \ y)) by BCIALG_1:2

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

.= (x \ y) \ y by BCIALG_1:8 ;

A10: (x \ (x \ (x \ y))) \ ((x \ y) \ x) = (x \ y) \ ((x \ y) \ x) by BCIALG_1:8

.= x \ y by A8, BCIALG_1:2 ;

(x \ (x \ (x \ y))) \ ((x \ y) \ x) = ((x,(x \ (x \ y))) to_power 1) \ ((x \ y) \ x) by BCIALG_2:2

.= ((((x \ y),((x \ y) \ x)) to_power 1),(x \ (x \ y))) to_power 1 by A7, BCIALG_2:2

.= (((x \ y) \ ((x \ y) \ x)),(x \ (x \ y))) to_power 1 by BCIALG_2:2

.= ((x \ y) \ ((x \ y) \ x)) \ (x \ (x \ y)) by BCIALG_2:2 ;

hence x \ y = (x \ y) \ y by A10, A9; :: thesis: verum