let X be BCI-algebra; :: thesis: for a, b being Element of AtomSet X
for x being Element of BranchV b holds a \ x = a \ b
let a, b be Element of AtomSet X; :: thesis: for x being Element of BranchV b holds a \ x = a \ b
let x be Element of BranchV b; :: thesis: a \ x = a \ b
a \ b in { x1 where x1 is Element of X : x1 is atom } ;
then A1: ex x1 being Element of X st
( a \ b = x1 & x1 is atom ) ;
x in { yy where yy is Element of X : b <= yy } ;
then A2: ex yy being Element of X st
( x = yy & b <= yy ) ;
(a \ x) \ (a \ b) = (a \ (a \ b)) \ x by Th7;
then (a \ x) \ (a \ b) = b \ x by Th24;
then (a \ x) \ (a \ b) = 0. X by A2;
hence a \ x = a \ b by A1; :: thesis: verum