let x be ExtReal; :: thesis: (x / 2) + (x / 2) = x
(x / 2) + (x / 2) = (x + x) / 2 by Th95
.= (2 * x) / 2 by Th94
.= x * (2 / 2) by Th66
.= x by Th81 ;
hence (x / 2) + (x / 2) = x ; :: thesis: verum