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;