let X be BCI-algebra; :: thesis: for a being Element of AtomSet X
for x, y being Element of BranchV a holds x \ y in BCK-part X
let a be Element of AtomSet X; :: thesis: for x, y being Element of BranchV a holds x \ y in BCK-part X
let x, y be Element of BranchV a; :: thesis: x \ y in BCK-part X
set b = a \ a;
( a \ a = 0. X & x \ y in BranchV (a \ a) ) by Def5, Th39;
hence x \ y in BCK-part X ; :: thesis: verum