let n be Element of NAT ; :: thesis: for X, Y being Subset of (TOP-REAL n)
for p being Point of (TOP-REAL n) holds (X + p) (o) Y = (X (o) Y) + p
let X, Y be Subset of (TOP-REAL n); :: thesis: for p being Point of (TOP-REAL n) holds (X + p) (o) Y = (X (o) Y) + p
let p be Point of (TOP-REAL n); :: thesis: (X + p) (o) Y = (X (o) Y) + p
thus (X + p) (o) Y = ((X (+) Y) + p) (-) Y by Th15
.= (X (o) Y) + p by Th14 ; :: thesis: verum