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 Th11;
hence f = g by Th10; :: thesis: verum