let X be BCI-algebra; :: thesis: for x being Element of X
for a, b being Element of AtomSet X holds a \ (x \ b) = b \ (x \ a)
let x be Element of X; :: thesis: for a, b being Element of AtomSet X holds a \ (x \ b) = b \ (x \ a)
let a, b be Element of AtomSet X; :: thesis: a \ (x \ b) = b \ (x \ a)
b in AtomSet X ;
then A1: ex y1 being Element of X st
( b = y1 & y1 is atom ) ;
(x \ (x \ b)) \ b = 0. X by BCIALG_1:1;
then (b \ (x \ a)) \ (a \ (x \ b)) = ((x \ (x \ b)) \ (x \ a)) \ (a \ (x \ b)) by A1;
then (b \ (x \ a)) \ (a \ (x \ b)) = ((x \ (x \ a)) \ (x \ b)) \ (a \ (x \ b)) by BCIALG_1:7;
then (b \ (x \ a)) \ (a \ (x \ b)) = (((x \ (x \ a)) \ (x \ b)) \ (a \ (x \ b))) \ (0. X) by BCIALG_1:2;
then (b \ (x \ a)) \ (a \ (x \ b)) = (((x \ (x \ a)) \ (x \ b)) \ (a \ (x \ b))) \ ((x \ (x \ a)) \ a) by BCIALG_1:1;
then A2: (b \ (x \ a)) \ (a \ (x \ b)) = 0. X by BCIALG_1:def 3;
a \ (x \ b) <= b \ (x \ a) by BCIALG_1:26;
then (a \ (x \ b)) \ (b \ (x \ a)) = 0. X ;
hence a \ (x \ b) = b \ (x \ a) by A2, BCIALG_1:def 7; :: thesis: verum