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

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