let x be ext-real number ; :: thesis: (x / 2) + (x / 2) = x
(x / 2) + (x / 2) = (x + x) / 2 by Th106
.= (2 * x) / 2 by Th12
.= x * (2 / 2) by Th6
.= x by Th79 ;
hence (x / 2) + (x / 2) = x ; :: thesis: verum