let x, y be Element of REAL+ ; :: thesis: x - y in REAL

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

suppose y <=' x ; :: thesis: x - y in REAL

then x - y = x -' y by ARYTM_1:def 2;
then x - y in REAL+ ;
hence x - y in REAL by Th1; :: thesis: verum

end;

suppose A1: not y <=' x ; :: thesis: x - y in REAL

then x - y = [{},(y -' x)] by ARYTM_1:def 2;
hence x - y in REAL by A1, Th2, ARYTM_1:9; :: thesis: verum

end;

end;