let p, q, r be Point of (TOP-REAL 3); :: thesis: ( p,q,r are_LinDep iff |{p,q,r}| = 0 )

hereby :: thesis: ( |{p,q,r}| = 0 implies p,q,r are_LinDep )

assume p,q,r are_LinDep ; :: thesis: |{p,q,r}| = 0
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 ANPROJ_1:def 2;
hence |{p,q,r}| = 0 by Th35; :: thesis: verum

end;

assume |{p,q,r}| = 0 ; :: thesis: 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; :: thesis: verum