let n be Element of NAT ; :: thesis: for X, Y being Subset of (TOP-REAL n) holds
( X (+) Y = (X (+) Y) (O) Y & X (-) Y = (X (-) Y) (o) Y )
let X, Y be Subset of (TOP-REAL n); :: thesis: ( X (+) Y = (X (+) Y) (O) Y & X (-) Y = (X (-) Y) (o) Y )
thus X (+) Y = (X (+) Y) (O) Y :: thesis: X (-) Y = (X (-) Y) (o) Y

proof

(X (+) Y) (O) Y = (X (o) Y) (+) Y ;
hence X (+) Y = (X (+) Y) (O) Y by Th50; :: thesis: verum

end;

(X (-) Y) (o) Y = (X (O) Y) (-) Y ;
hence X (-) Y = (X (-) Y) (o) Y by Th50; :: thesis: verum