theorem Th7: :: RLAFFIN3:7

for n, k being Nat
for An being Subset of (TOP-REAL n)
for Ak being Subset of (TOP-REAL k) st k <= n & An = { v where v is Element of (TOP-REAL n) : v | k in Ak } holds
( An is open iff Ak is open )