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 Th105
.= x * (2 / 2) by Th77
.= x by Th92 ;
hence (x / 2) + (x / 2) = x ; :: thesis: verum