let r be Real; :: thesis: for f, g being ExtReal st r - f = r - g holds
f = g
let f, g be ExtReal; :: thesis: ( r - f = r - g implies f = g )
assume r - f = r - g ; :: thesis: f = g
then - f = - g by Th11;
hence f = g by Th10; :: thesis: verum