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

for x being Element of BranchV a holds a \ x = 0. X

let a be Element of AtomSet X; :: thesis: for x being Element of BranchV a holds a \ x = 0. X

let x be Element of BranchV a; :: thesis: a \ x = 0. X

x in { x1 where x1 is Element of X : a <= x1 } ;

then ex x1 being Element of X st

( x = x1 & a <= x1 ) ;

hence a \ x = 0. X ; :: thesis: verum

for x being Element of BranchV a holds a \ x = 0. X

let a be Element of AtomSet X; :: thesis: for x being Element of BranchV a holds a \ x = 0. X

let x be Element of BranchV a; :: thesis: a \ x = 0. X

x in { x1 where x1 is Element of X : a <= x1 } ;

then ex x1 being Element of X st

( x = x1 & a <= x1 ) ;

hence a \ x = 0. X ; :: thesis: verum