let a, b be complex number ; :: thesis: ((a / (3 * b)) + (a / (3 * b))) + (a / (3 * b)) = a / b
thus ((a / (3 * b)) + (a / (3 * b))) + (a / (3 * b)) = ((a + a) / (3 * b)) + (a / (3 * b)) by Th63
.= ((a + a) + a) / (3 * b) by Th63
.= (3 * a) / (3 * b)
.= a / b by Lm11 ; :: thesis: verum