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)
A1: b in AtomSet X ;
consider y1 being Element of X such that
A3: ( b = y1 & y1 is atom ) by A1;
a \ (x \ b) <= b \ (x \ a) by BCIALG_1:26;
then A5: (a \ (x \ b)) \ (b \ (x \ a)) = 0. X by BCIALG_1:def 11;
(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 A3, BCIALG_1:def 14;
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 (b \ (x \ a)) \ (a \ (x \ b)) = 0. X by BCIALG_1:def 3;
hence a \ (x \ b) = b \ (x \ a) by A5, BCIALG_1:def 7; :: thesis: verum