let X be BCI-algebra; :: thesis: ( X is p-Semisimple iff for x, y being Element of X st x \ y = 0. X holds

x = y )

thus ( X is p-Semisimple implies for x, y being Element of X st x \ y = 0. X holds

x = y ) :: thesis: ( ( for x, y being Element of X st x \ y = 0. X holds

x = y ) implies X is p-Semisimple )

x = y ; :: thesis: X is p-Semisimple

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

x = y )

thus ( X is p-Semisimple implies for x, y being Element of X st x \ y = 0. X holds

x = y ) :: thesis: ( ( for x, y being Element of X st x \ y = 0. X holds

x = y ) implies X is p-Semisimple )

proof

assume A3:
for x, y being Element of X st x \ y = 0. X holds
assume A1:
X is p-Semisimple
; :: thesis: for x, y being Element of X st x \ y = 0. X holds

x = y

for x, y being Element of X st x \ y = 0. X holds

x = y

x = y ; :: thesis: verum

end;x = y

for x, y being Element of X st x \ y = 0. X holds

x = y

proof

hence
for x, y being Element of X st x \ y = 0. X holds
let x, y be Element of X; :: thesis: ( x \ y = 0. X implies x = y )

assume A2: x \ y = 0. X ; :: thesis: x = y

(0. X) \ (x \ y) = (y \ x) \ ((0. X) `) by A1, BCIALG_1:66

.= (y \ x) \ (0. X) by BCIALG_1:def 5

.= y \ x by BCIALG_1:2 ;

then y \ x = 0. X by A2, BCIALG_1:def 5;

hence x = y by A2, BCIALG_1:def 7; :: thesis: verum

end;assume A2: x \ y = 0. X ; :: thesis: x = y

(0. X) \ (x \ y) = (y \ x) \ ((0. X) `) by A1, BCIALG_1:66

.= (y \ x) \ (0. X) by BCIALG_1:def 5

.= y \ x by BCIALG_1:2 ;

then y \ x = 0. X by A2, BCIALG_1:def 5;

hence x = y by A2, BCIALG_1:def 7; :: thesis: verum

x = y ; :: thesis: verum

x = y ; :: thesis: X is p-Semisimple

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

proof

hence
X is p-Semisimple
; :: thesis: verum
let x, y be Element of X; :: thesis: x \ (x \ y) = y

(x \ (x \ y)) \ y = (x \ y) \ (x \ y) by BCIALG_1:7

.= 0. X by BCIALG_1:def 5 ;

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

end;(x \ (x \ y)) \ y = (x \ y) \ (x \ y) by BCIALG_1:7

.= 0. X by BCIALG_1:def 5 ;

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