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;