for n being Nat
for X being set holds
( X is affinely-independent Subset of (REAL-NS n) iff X is affinely-independent Subset of (TOP-REAL n) )