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 consider x1 being Element of X such that
A1: ( x = x1 & a <= x1 ) ;
thus a \ x = 0. X by A1, Def11; :: thesis: verum