let x, y, z be Element of REAL+ ; :: thesis: ( x + y = x + z implies y = z )
assume A1: x + y = x + z ; :: thesis: y = z
consider q being Element of REAL+ such that
A2: ( z + q = y or y + q = z ) by Th10;

per cases ( z + q = y or y + q = z ) by A2;

suppose A3: z + q = y ; :: thesis: y = z

then x + y = (x + y) + q by A1, Th6;
then q = {} by Lm35;
hence y = z by A3, Def8; :: thesis: verum

end;

suppose A4: y + q = z ; :: thesis: y = z

then x + z = (x + z) + q by A1, Th6;
then q = {} by Lm35;
hence y = z by A4, Def8; :: thesis: verum

end;

end;