let n be Element of NAT ; :: thesis: for X, Y being Subset of (TOP-REAL n) st Y = {} holds
X (-) Y = REAL n
let X, Y be Subset of (TOP-REAL n); :: thesis: ( Y = {} implies X (-) Y = REAL n )
assume A1: Y = {} ; :: thesis: X (-) Y = REAL n
{ y where y is Point of (TOP-REAL n) : Y + y c= X } = REAL n

proof

thus { y where y is Point of (TOP-REAL n) : Y + y c= X } c= REAL n :: according to XBOOLE_0:def 10 :: thesis: REAL n c= { y where y is Point of (TOP-REAL n) : Y + y c= X }

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { y where y is Point of (TOP-REAL n) : Y + y c= X } or x in REAL n )
assume x in { y where y is Point of (TOP-REAL n) : Y + y c= X } ; :: thesis: x in REAL n
then consider y being Point of (TOP-REAL n) such that
A2: ( x = y & Y + y c= X ) ;
x in the carrier of (TOP-REAL n) by A2;
hence x in REAL n by EUCLID:25; :: thesis: verum

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in REAL n or x in { y where y is Point of (TOP-REAL n) : Y + y c= X } )
assume x in REAL n ; :: thesis: x in { y where y is Point of (TOP-REAL n) : Y + y c= X }
then reconsider a = x as Point of (TOP-REAL n) by EUCLID:25;
Y + a = {} by A1, Th4;
then Y + a c= X by XBOOLE_1:2;
hence x in { y where y is Point of (TOP-REAL n) : Y + y c= X } ; :: thesis: verum

end;

hence X (-) Y = REAL n ; :: thesis: verum