let x, y, z be Element of REAL+ ; :: thesis: ( x = y + z implies z <=' x )
reconsider zz = {} as Element of REAL+ by Th1;
assume A1: x = y + z ; :: thesis: z <=' x
assume A2: not z <=' x ; :: thesis: contradiction
then consider y0 being Element of REAL+ such that
A3: x + y0 = z by Th9;
x = x + (y + y0) by A1, A3, Th6;
then x + zz = x + (y + y0) by Def8;
then y0 = {} by Th5, Th11;
then z = x by A3, Def8;
hence contradiction by A2; :: thesis: verum