let f, g be ExtReal; :: thesis: {f} -- {g} = {(f - g)}
thus {f} -- {g} = {f} ++ {(- g)} by Th9
.= {(f - g)} by Th43 ; :: thesis: verum