theorem Th25: :: RLAFFIN3:25

for n, k being Nat
for Affn being affinely-independent Subset of (TOP-REAL n)
for Ak being Subset of (TOP-REAL k)
for EN being Enumeration of Affn
for An being Subset of (TOP-REAL n) st k <= n & card Affn = n + 1 & An = { pn where pn is Point of (TOP-REAL n) : (pn |-- EN) | k in Ak } holds
( Ak is open iff An is open )