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 holds x \ y in BranchV (a \ b)

let a, b be Element of AtomSet X; :: thesis: for x being Element of BranchV a

for y being Element of BranchV b holds x \ y in BranchV (a \ b)

let x be Element of BranchV a; :: thesis: for y being Element of BranchV b holds x \ y in BranchV (a \ b)

let y be Element of BranchV b; :: thesis: x \ y in BranchV (a \ b)

(a \ b) \ (x \ y) = (((a \ b) `) `) \ (x \ y) by Th29;

then (a \ b) \ (x \ y) = ((x \ y) `) \ ((a \ b) `) by Th7;

then (a \ b) \ (x \ y) = ((x `) \ (y `)) \ ((a \ b) `) by Th9;

then (a \ b) \ (x \ y) = ((x `) \ ((a \ b) `)) \ (y `) by Th7;

then (a \ b) \ (x \ y) = ((((a \ b) `) `) \ x) \ (y `) by Th7;

then (a \ b) \ (x \ y) = ((a \ b) \ x) \ (y `) by Th29;

then (a \ b) \ (x \ y) = ((a \ x) \ b) \ (y `) by Th7;

then (a \ b) \ (x \ y) = (b `) \ (y `) by Lm2;

then (a \ b) \ (x \ y) = (b \ y) ` by Th9;

then (a \ b) \ (x \ y) = (0. X) ` by Lm2;

then (a \ b) \ (x \ y) = 0. X by Def5;

then a \ b <= x \ y ;

hence x \ y in BranchV (a \ b) ; :: thesis: verum

for x being Element of BranchV a

for y being Element of BranchV b holds x \ y in BranchV (a \ b)

let a, b be Element of AtomSet X; :: thesis: for x being Element of BranchV a

for y being Element of BranchV b holds x \ y in BranchV (a \ b)

let x be Element of BranchV a; :: thesis: for y being Element of BranchV b holds x \ y in BranchV (a \ b)

let y be Element of BranchV b; :: thesis: x \ y in BranchV (a \ b)

(a \ b) \ (x \ y) = (((a \ b) `) `) \ (x \ y) by Th29;

then (a \ b) \ (x \ y) = ((x \ y) `) \ ((a \ b) `) by Th7;

then (a \ b) \ (x \ y) = ((x `) \ (y `)) \ ((a \ b) `) by Th9;

then (a \ b) \ (x \ y) = ((x `) \ ((a \ b) `)) \ (y `) by Th7;

then (a \ b) \ (x \ y) = ((((a \ b) `) `) \ x) \ (y `) by Th7;

then (a \ b) \ (x \ y) = ((a \ b) \ x) \ (y `) by Th29;

then (a \ b) \ (x \ y) = ((a \ x) \ b) \ (y `) by Th7;

then (a \ b) \ (x \ y) = (b `) \ (y `) by Lm2;

then (a \ b) \ (x \ y) = (b \ y) ` by Th9;

then (a \ b) \ (x \ y) = (0. X) ` by Lm2;

then (a \ b) \ (x \ y) = 0. X by Def5;

then a \ b <= x \ y ;

hence x \ y in BranchV (a \ b) ; :: thesis: verum