let p, q, r be Point of (TOP-REAL 3); ( |{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
; 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; verum