let x, y be Element of REAL+ ; :: thesis: ( x <=' y & y -' x = {} implies x = y )
assume A1: x <=' y ; :: thesis: ( not y -' x = {} or x = y )
assume y -' x = {} ; :: thesis: x = y
then y <=' x by Th9;
hence x = y by A1, Th4; :: thesis: verum