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

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