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 by Def11;
hence x \ y in BranchV (a \ b) ; :: thesis: verum