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