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) )

A1: ( X is semi-Brouwerian-algebra implies X is positive-implicative BCK-Algebra_with_Condition(S) )

proof

( X is positive-implicative BCK-Algebra_with_Condition(S) implies X is semi-Brouwerian-algebra )
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

end;A3: for x, y being Element of X st x \ y = 0. X & y \ x = 0. X holds

x = y

proof

A7:
for x, y, z being Element of X holds (x \ y) \ z = (x \ z) \ y
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;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

proof

A8:
for x, y, z being Element of X holds ((x \ y) \ z) \ ((x \ z) \ y) = 0. X
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;(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

proof

A9:
for x, y being Element of X holds x * y = x * (y \ x)
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;((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

proof

A10:
for x being Element of X holds x ` = 0. X
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;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

proof

for x, y, z being Element of X holds ((x \ y) \ (z \ y)) \ (x \ z) = 0. X
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;(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

proof

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
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;((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

proof

hence
( X is positive-implicative BCK-Algebra_with_Condition(S) iff X is semi-Brouwerian-algebra )
by A1; :: thesis: verum
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

hence X is semi-Brouwerian-algebra by A11, A12, Def12, Def13, Def14; :: thesis: verum

end;A12: for x, y being Element of X holds (x \ y) * y = x * y

proof

( ( 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;
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;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

hence X is semi-Brouwerian-algebra by A11, A12, Def12, Def13, Def14; :: thesis: verum