let X be BCI-algebra; :: thesis: for a being Element of X

for x, b being Element of AtomSet X st x is Element of BranchV b holds

a \ x = a \ b

set P = AtomSet X;

let a be Element of X; :: thesis: for x, b being Element of AtomSet X st x is Element of BranchV b holds

a \ x = a \ b

let x, b be Element of AtomSet X; :: thesis: ( x is Element of BranchV b implies a \ x = a \ b )

set B = BranchV b;

assume x is Element of BranchV b ; :: thesis: a \ x = a \ b

then x in BranchV b ;

then ex x3 being Element of X st

( x = x3 & b <= x3 ) ;

then A1: b \ x = 0. X ;

x in { x1 where x1 is Element of X : x1 is minimal } ;

then ex x1 being Element of X st

( x = x1 & x1 is minimal ) ;

hence a \ x = a \ b by A1; :: thesis: verum

for x, b being Element of AtomSet X st x is Element of BranchV b holds

a \ x = a \ b

set P = AtomSet X;

let a be Element of X; :: thesis: for x, b being Element of AtomSet X st x is Element of BranchV b holds

a \ x = a \ b

let x, b be Element of AtomSet X; :: thesis: ( x is Element of BranchV b implies a \ x = a \ b )

set B = BranchV b;

assume x is Element of BranchV b ; :: thesis: a \ x = a \ b

then x in BranchV b ;

then ex x3 being Element of X st

( x = x3 & b <= x3 ) ;

then A1: b \ x = 0. X ;

x in { x1 where x1 is Element of X : x1 is minimal } ;

then ex x1 being Element of X st

( x = x1 & x1 is minimal ) ;

hence a \ x = a \ b by A1; :: thesis: verum