assume A1: X is BCI-commutative ; :: thesis: for a being Element of AtomSet X
for x, y being Element of BranchV a holds x \ (x \ y) = y \ (y \ x)
let a be Element of AtomSet X; :: thesis: for x, y being Element of BranchV a holds x \ (x \ y) = y \ (y \ x)
let x, y be Element of BranchV a; :: thesis: x \ (x \ y) = y \ (y \ x)
y \ x in BranchV (a \ a) by BCIALG_1:39;
then ex z1 being Element of X st
( y \ x = z1 & a \ a <= z1 ) ;
then 0. X <= y \ x by BCIALG_1:def 5;
then (0. X) \ (y \ x) = 0. X ;
then A2: (y \ (y \ x)) \ (x \ (x \ y)) = 0. X by A1, Th17;
x \ y in BranchV (a \ a) by BCIALG_1:39;
then ex z being Element of X st
( x \ y = z & a \ a <= z ) ;
then 0. X <= x \ y by BCIALG_1:def 5;
then (0. X) \ (x \ y) = 0. X ;
then (x \ (x \ y)) \ (y \ (y \ x)) = 0. X by A1, Th17;
hence x \ (x \ y) = y \ (y \ x) by A2, BCIALG_1:def 7; :: thesis: verum

let x, y be Element of X; :: thesis: ( x \ y = 0. X implies x = y \ (y \ x) )
set aa = (0. X) \ ((0. X) \ x);
(((0. X) \ ((0. X) \ x)) `) ` = (0. X) \ ((0. X) \ x) by BCIALG_1:8;
then A4: (0. X) \ ((0. X) \ x) in AtomSet X by BCIALG_1:29;
A5: ((0. X) \ ((0. X) \ x)) \ x = ((0. X) \ x) \ ((0. X) \ x) by BCIALG_1:7
.= 0. X by BCIALG_1:def 5 ;
then A6: (0. X) \ ((0. X) \ x) <= x ;
assume A7: x \ y = 0. X ; :: thesis: x = y \ (y \ x)
then ((0. X) \ ((0. X) \ x)) \ y = 0. X by A5, BCIALG_1:3;
then (0. X) \ ((0. X) \ x) <= y ;
then consider aa being Element of AtomSet X such that
A8: ( aa <= x & aa <= y ) by A4, A6;
( x in BranchV aa & y in BranchV aa ) by A8;
then x \ (x \ y) = y \ (y \ x) by A3;
hence x = y \ (y \ x) by A7, BCIALG_1:2; :: thesis: verum