let p, q, r be Point of (TOP-REAL 3); :: thesis: 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
let M be Matrix of 3,F_Real; :: thesis: 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
let pt, qt, rt be FinSequence of 1 -tuples_on REAL; :: thesis: ( M = <*(M2F pt),(M2F qt),(M2F rt)*> & Det M = 0 & M2F pt = p & M2F qt = q & M2F rt = r implies |{p,q,r}| = 0 )
assume that
A1: M = <*(M2F pt),(M2F qt),(M2F rt)*> and
A2: Det M = 0 and
A3: M2F pt = p and
A4: M2F qt = q and
A5: M2F rt = r ; :: thesis: |{p,q,r}| = 0
( p = <*(p `1),(p `2),(p `3)*> & q = <*(q `1),(q `2),(q `3)*> & r = <*(r `1),(r `2),(r `3)*> ) by EUCLID_5:3;
hence |{p,q,r}| = 0 by A2, A1, A3, A4, A5, Th29; :: thesis: verum