let r be real number ; :: thesis: for f, g being ext-real number st r - f = r - g holds
f = g
let f, g be ext-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 ThM3; :: thesis: verum