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

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

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

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

proof

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

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

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

proof

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

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

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

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

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

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

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

end;A2: (x \ (x \ y)) \ (x \ y) = y \ (y \ x) by A1, BCIALG_3:35;

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

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

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

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

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

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

proof

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

A4: Polynom (1,0,x,y) = Polynom (0,0,y,x) by A3, Def3;

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

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

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

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

hence (x \ (x \ y)) \ (x \ y) = y \ (y \ x) ; :: thesis: verum

end;A4: Polynom (1,0,x,y) = Polynom (0,0,y,x) by A3, Def3;

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

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

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

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

hence (x \ (x \ y)) \ (x \ y) = y \ (y \ x) ; :: thesis: verum