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 )proof
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
proof
let x,
y be
Element of
X;
:: thesis: Polynom 1,0 ,x,y = Polynom 0 ,0 ,y,x
B1:
(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 B1, 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;
hence
X is
BCK-algebra of 1,
0 ,
0 ,
0
by A1, Def2;
:: thesis: verum
end;
assume A1:
X is BCK-algebra of 1, 0 , 0 , 0
; :: thesis: X is BCK-implicative BCK-algebra
for x, y being Element of X holds (x \ (x \ y)) \ (x \ y) = y \ (y \ x)
proof
let x,
y be
Element of
X;
:: thesis: (x \ (x \ y)) \ (x \ y) = y \ (y \ x)
B1:
Polynom 1,
0 ,
x,
y = Polynom 0 ,
0 ,
y,
x
by A1, Def2;
(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 B1, BCIALG_2:1
.=
y \ (y \ x)
by BCIALG_2:2
;
hence
(x \ (x \ y)) \ (x \ y) = y \ (y \ x)
;
:: thesis: verum
end;
hence
X is BCK-implicative BCK-algebra
by A1, BCIALG_3:35; :: thesis: verum