let f, g be ext-real number ; :: thesis: for r being real number st r - f = r - g holds
f = g
let r be real number ; :: thesis: ( r - f = r - g implies f = g )
assume r - f = r - g ; :: thesis: f = g
then - f = - g by Th4;
hence f = g by Th3; :: thesis: verum