let x, y, z be Element of REAL+ ; :: thesis: ( z -' y <=' x iff z <=' x + y )

per cases ( y <=' z or not y <=' z ) ;

suppose y <=' z ; :: thesis: ( z -' y <=' x iff z <=' x + y )

then (z -' y) + y = z by Def1;
hence ( z -' y <=' x iff z <=' x + y ) by Th7; :: thesis: verum

end;

suppose A1: not y <=' z ; :: thesis: ( z -' y <=' x iff z <=' x + y )

A2: y <=' x + y by ARYTM_2:19;
z -' y = {} by A1, Def1;
hence ( z -' y <=' x iff z <=' x + y ) by A1, A2, Th3, Th6; :: thesis: verum

end;

end;