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;
A1: a \ a = 0. X by Def5;
x \ y in BranchV (a \ a) by Th39;
hence x \ y in BCK-part X by A1; :: thesis: verum