theorem Th34:
for
p,
q,
r being
Point of
(TOP-REAL 3) for
M being
Matrix of 3,
F_Real st
M = <*<*(p `1),(p `2),(p `3)*>,<*(q `1),(q `2),(q `3)*>,<*(r `1),(r `2),(r `3)*>*> &
the_rank_of M < 3 holds
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 ) )