let p, q, r be Point of (TOP-REAL 3); ( p,q,r are_LinDep iff |{p,q,r}| = 0 )
assume
|{p,q,r}| = 0
; p,q,r are_LinDep
then
ex a, b, c being Real st
( ((a * p) + (b * q)) + (c * r) = 0. (TOP-REAL 3) & ( a <> 0 or b <> 0 or c <> 0 ) )
by Th36;
hence
p,q,r are_LinDep
by ANPROJ_1:def 2; verum