let X be non empty BCIStr_1 ; :: thesis: ( X is positive-implicative BCK-Algebra_with_Condition(S) iff X is semi-Brouwerian-algebra )
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: X is positive-implicative BCK-Algebra_with_Condition(S)
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 A2, Def12
.= (x \ x) * x by A2, Def14
.= (0. X) * x by A2, BCIALG_1:def 5
.= y * x by A2, A5, Def14 ;
y = y * y by A2, Def12
.= (y \ y) * y by A2, Def14
.= y * (y \ y) by A2, Def13
.= y * (0. X) by A2, BCIALG_1:def 5
.= (x \ y) * y by A2, A4, Def13
.= x * y by A2, Def14 ;
hence x = y by A2, A6, Def13; :: 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 A2, Def2
.= x \ (z * y) by A2, Def13 ;
hence (x \ y) \ z = (x \ z) \ y by A2, Def2; :: 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 A2, BCIALG_1:def 5; :: 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 A2, Def13
.= y * x by A2, Def14 ;
hence x * y = x * (y \ x) by A2, Def13; :: 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 A2, BCIALG_1:def 5
.= x \ (x * x) by A2, Def2
.= x \ x by A2, Def12
.= 0. X by A2, BCIALG_1:def 5 ;
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 A2, Def2
.= (x \ ((z \ y) * y)) \ (x \ z) by A2, Def13
.= (x \ (z * y)) \ (x \ z) by A2, Def14
.= ((x \ z) \ y) \ (x \ z) by A2, Def2
.= ((x \ z) \ (x \ z)) \ y by A7
.= y ` by A2, BCIALG_1:def 5 ;
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 A2, A10, A3, A8, A9, Th47, BCIALG_1:def 3, BCIALG_1:def 4, BCIALG_1:def 7, BCIALG_1:def 8; :: 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: X is semi-Brouwerian-algebra
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 A11, Th47;
then x * y = y * (x \ y) by A11, Th6;
hence (x \ y) * y = x * y by A11, Th6; :: 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 A11, Th6, Th44;
hence X is semi-Brouwerian-algebra by A11, A12, Def12, Def13, Def14; :: thesis: verum
end;
hence ( X is positive-implicative BCK-Algebra_with_Condition(S) iff X is semi-Brouwerian-algebra ) by A1; :: thesis: verum