let p, q, r be 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
let M be 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 pt, qt, rt be FinSequence of 1 -tuples_on REAL; ( 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
; |{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; verum