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