let X be non empty BCIStr_1 ; :: thesis:
A1: ( X is semi-Brouwerian-algebra implies X is positive-implicative BCK-Algebra_with_Condition(S) )
proof
assume A2: X is semi-Brouwerian-algebra ; :: thesis:
A3: for x, y being Element of X st x \ y = 0. X & y \ x = 0. X holds
x = y
proof
let x, y be Element of X; :: thesis: ( x \ y = 0. X & y \ x = 0. X implies x = y )
assume that
A4: x \ y = 0. X and
A5: y \ x = 0. X ; :: thesis: x = y
A6: x = x * x by
.= (x \ x) * x by
.= (0. X) * x by
.= y * x by ;
y = y * y by
.= (y \ y) * y by
.= y * (y \ y) by
.= y * (0. X) by
.= (x \ y) * y by
.= x * y by ;
hence x = y by ; :: thesis: verum
end;
A7: for x, y, z being Element of X holds (x \ y) \ z = (x \ z) \ y
proof
let x, y, z be Element of X; :: thesis: (x \ y) \ z = (x \ z) \ y
(x \ y) \ z = x \ (y * z) by
.= x \ (z * y) by ;
hence (x \ y) \ z = (x \ z) \ y by ; :: thesis: verum
end;
A8: for x, y, z being Element of X holds ((x \ y) \ z) \ ((x \ z) \ y) = 0. X
proof
let x, y, z be Element of X; :: thesis: ((x \ y) \ z) \ ((x \ z) \ y) = 0. X
((x \ y) \ z) \ ((x \ z) \ y) = ((x \ y) \ z) \ ((x \ y) \ z) by A7;
hence ((x \ y) \ z) \ ((x \ z) \ y) = 0. X by ; :: thesis: verum
end;
A9: for x, y being Element of X holds x * y = x * (y \ x)
proof
let x, y be Element of X; :: thesis: x * y = x * (y \ x)
x * (y \ x) = (y \ x) * x by
.= y * x by ;
hence x * y = x * (y \ x) by ; :: thesis: verum
end;
A10: for x being Element of X holds x ` = 0. X
proof
let x be Element of X; :: thesis: x ` = 0. X
(0. X) \ x = (x \ x) \ x by
.= x \ (x * x) by
.= x \ x by
.= 0. X by ;
hence x ` = 0. X ; :: thesis: verum
end;
for x, y, z being Element of X holds ((x \ y) \ (z \ y)) \ (x \ z) = 0. X
proof
let x, y, z be Element of X; :: thesis: ((x \ y) \ (z \ y)) \ (x \ z) = 0. X
((x \ y) \ (z \ y)) \ (x \ z) = (x \ (y * (z \ y))) \ (x \ z) by
.= (x \ ((z \ y) * y)) \ (x \ z) by
.= (x \ (z * y)) \ (x \ z) by
.= ((x \ z) \ y) \ (x \ z) by
.= ((x \ z) \ (x \ z)) \ y by A7
.= y ` by ;
hence ((x \ y) \ (z \ y)) \ (x \ z) = 0. X by A10; :: thesis: verum
end;
hence X is positive-implicative BCK-Algebra_with_Condition(S) by ; :: thesis: verum
end;
( X is positive-implicative BCK-Algebra_with_Condition(S) implies X is semi-Brouwerian-algebra )
proof
assume A11: X is positive-implicative BCK-Algebra_with_Condition(S) ; :: thesis:
A12: for x, y being Element of X holds (x \ y) * y = x * y
proof
let x, y be Element of X; :: thesis: (x \ y) * y = x * y
y * x = y * (x \ y) by ;
then x * y = y * (x \ y) by ;
hence (x \ y) * y = x * y by ; :: thesis: verum
end;
( ( for x being Element of X holds x * x = x ) & ( for x, y being Element of X holds x * y = y * x ) ) by ;
hence X is semi-Brouwerian-algebra by ; :: thesis: verum
end;
hence ( X is positive-implicative BCK-Algebra_with_Condition(S) iff X is semi-Brouwerian-algebra ) by A1; :: thesis: verum