let x, y be Element of REAL+ ; :: thesis: ( x = {} & y <> {} implies x - y = [{} ,y] )
assume A1: ( x = {} & y <> {} ) ; :: thesis: x - y = [{} ,y]
then x <=' y by Th6;
then not y <=' x by A1, Th4;
hence x - y = [{} ,(y -' x)] by Def2
.= [{} ,y] by A1, Lm4 ;
:: thesis: verum