theorem Th45: :: REAL_NS2:45

for n being Nat
for Ar being Subset of (REAL-NS n)
for At being Subset of (TOP-REAL n)
for v being Element of (REAL-NS n)
for w being Element of (TOP-REAL n) st Ar = At & v = w & v in Affin Ar & Ar is affinely-independent holds
v |-- Ar = w |-- At