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

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