let X be BCI-algebra; :: thesis: for a, b being Element of AtomSet X
for x being Element of BranchV a
for y being Element of BranchV b st a <> b holds
not x \ y in BCK-part X
let a, b be Element of AtomSet X; :: thesis: for x being Element of BranchV a
for y being Element of BranchV b st a <> b holds
not x \ y in BCK-part X
let x be Element of BranchV a; :: thesis: for y being Element of BranchV b st a <> b holds
not x \ y in BCK-part X
let y be Element of BranchV b; :: thesis: ( a <> b implies not x \ y in BCK-part X )
assume A1: a <> b ; :: thesis: not x \ y in BCK-part X
x \ y in BranchV (a \ b) by Th39;
then ex xy being Element of X st
( x \ y = xy & a \ b <= xy ) ;
then (a \ b) \ (x \ y) = 0. X ;
then (a \ (x \ y)) \ b = 0. X by Th7;
then (a \ (x \ y)) \ ((a \ (x \ y)) \ b) = a \ (x \ y) by Th2;
then A2: b = a \ (x \ y) by Th24;
assume x \ y in BCK-part X ; :: thesis: contradiction
hence contradiction by A1, A2, Th38; :: thesis: verum