theorem Th8: :: RLAFFIN3:8

for n, k being Nat
for Ak being Subset of (TOP-REAL k)
for A being Subset of (TOP-REAL (k + n)) st A = { (v ^ (n |-> 0)) where v is Element of (TOP-REAL k) : verum } holds
for B being Subset of ((TOP-REAL (k + n)) | A) st B = { v where v is Point of (TOP-REAL (k + n)) : ( v | k in Ak & v in A ) } holds
( Ak is open iff B is open )