theorem :: ANPROJ_8:96

for p, q, r being Point of (TOP-REAL 3)
for M being Matrix of 3,F_Real
for pt, qt, rt being FinSequence of 1 -tuples_on REAL st M = <*(M2F pt),(M2F qt),(M2F rt)*> & Det M = 0 & M2F pt = p & M2F qt = q & M2F rt = r holds
|{p,q,r}| = 0