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