let p, q, r be Point of (TOP-REAL 3); :: thesis: ( |{p,q,r}| = 0 implies 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 ) ) )
assume A1: |{p,q,r}| = 0 ; :: thesis: 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 ) )
reconsider M = <*<*(p `1),(p `2),(p `3)*>,<*(q `1),(q `2),(q `3)*>,<*(r `1),(r `2),(r `3)*>*> as Matrix of 3,F_Real by Th16;
Det M = 0 by A1, Th29
.= 0. F_Real by STRUCT_0:def 6 ;
then the_rank_of M < 3 by Th30;
hence 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 Th34; :: thesis: verum