let X be BCI-algebra; :: thesis: ( X is BCI-commutative iff for a being Element of AtomSet X
for x, y being Element of BranchV a holds x \ (x \ y) = y \ (y \ x) )
thus ( X is BCI-commutative implies for a being Element of AtomSet X
for x, y being Element of BranchV a holds x \ (x \ y) = y \ (y \ x) ) :: thesis: ( ( for a being Element of AtomSet X
for x, y being Element of BranchV a holds x \ (x \ y) = y \ (y \ x) ) implies X is BCI-commutative )

proof

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)
x \ y in BranchV (a \ a) by BCIALG_1:39;
then consider z being Element of X such that
A2: ( x \ y = z & a \ a <= z ) ;
0. X <= x \ y by A2, BCIALG_1:def 5;
then (0. X) \ (x \ y) = 0. X by BCIALG_1:def 11;
then A3: (x \ (x \ y)) \ (y \ (y \ x)) = 0. X by A1, Th17;
y \ x in BranchV (a \ a) by BCIALG_1:39;
then consider z1 being Element of X such that
A4: ( y \ x = z1 & a \ a <= z1 ) ;
0. X <= y \ x by A4, BCIALG_1:def 5;
then (0. X) \ (y \ x) = 0. X by BCIALG_1:def 11;
then (y \ (y \ x)) \ (x \ (x \ y)) = 0. X by A1, Th17;
hence x \ (x \ y) = y \ (y \ x) by A3, BCIALG_1:def 7; :: thesis: verum

end;

assume A5: for a being Element of AtomSet X
for x, y being Element of BranchV a holds x \ (x \ y) = y \ (y \ x) ; :: thesis: X is BCI-commutative
for x, y being Element of X st x \ y = 0. X holds
x = y \ (y \ x)

proof

let x, y be Element of X; :: thesis: ( x \ y = 0. X implies x = y \ (y \ x) )
assume A6: x \ y = 0. X ; :: thesis: 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 A7: (0. X) \ ((0. X) \ x) in AtomSet X by BCIALG_1:29;
A8: ((0. X) \ ((0. X) \ x)) \ x = ((0. X) \ x) \ ((0. X) \ x) by BCIALG_1:7
.= 0. X by BCIALG_1:def 5 ;
then ((0. X) \ ((0. X) \ x)) \ y = 0. X by A6, BCIALG_1:3;
then A9: (0. X) \ ((0. X) \ x) <= y by BCIALG_1:def 11;
(0. X) \ ((0. X) \ x) <= x by A8, BCIALG_1:def 11;
then consider aa being Element of AtomSet X such that
A10: ( aa <= x & aa <= y ) by A7, A9;
( x in BranchV aa & y in BranchV aa ) by A10;
then x \ (x \ y) = y \ (y \ x) by A5;
hence x = y \ (y \ x) by A6, BCIALG_1:2; :: thesis: verum

end;

hence X is BCI-commutative by Def4; :: thesis: verum