for n being Element of NAT
for q1, q2 being Point of (TOP-REAL n) st q1,q2 are_lindependent2 holds
( q1 <> q2 & q1 <> 0. (TOP-REAL n) & q2 <> 0. (TOP-REAL n) )