proof

assume A1: p,q,r are_collinear ; :: thesis:
consider up, vp being Element of (TOP-REAL 3), ufp being FinSequence of F_Real, pp being FinSequence of 1 -tuples_on REAL such that
A2: p = Dir up and
A3: not up is zero and
A4: up = ufp and
A5: pp = N * ufp and
A6: vp = M2F pp and
not vp is zero and
A7: (homography N) . p = Dir vp by DEF4;
consider uq, vq being Element of (TOP-REAL 3), ufq being FinSequence of F_Real, pq being FinSequence of 1 -tuples_on REAL such that
A8: q = Dir uq and
A9: not uq is zero and
A10: uq = ufq and
A11: pq = N * ufq and
A12: vq = M2F pq and
not vq is zero and
A13: (homography N) . q = Dir vq by DEF4;
consider ur, vr being Element of (TOP-REAL 3), ufr being FinSequence of F_Real, pr being FinSequence of 1 -tuples_on REAL such that
A14: r = Dir ur and
A15: not ur is zero and
A16: ur = ufr and
A17: pr = N * ufr and
A18: vr = M2F pr and
not vr is zero and
A19: (homography N) . r = Dir vr by DEF4;
consider u, v, w being Element of (TOP-REAL 3) such that
A20: p = Dir u and
A21: q = Dir v and
A22: r = Dir w and
A23: not u is zero and
A24: not v is zero and
A25: not w is zero and
A26: u,v,w are_LinDep by A1, ANPROJ_2:23;
A27: |{u,v,w}| = 0 by A26, Th37;
are_Prop up,u by A20, A2, A23, A3, ANPROJ_1:22;
then consider ap being Real such that
ap <> 0 and
A28: up = ap * u by ANPROJ_1:1;
are_Prop uq,v by A8, A21, A24, A9, ANPROJ_1:22;
then consider aq being Real such that
aq <> 0 and
A29: uq = aq * v by ANPROJ_1:1;
are_Prop ur,w by A22, A14, A25, A15, ANPROJ_1:22;
then consider ar being Real such that
ar <> 0 and
A30: ur = ar * w by ANPROJ_1:1;
A31: |{up,uq,ur}| = ap * |{u,(aq * v),(ar * w)}| by Th26, A28, A29, A30
.= ap * (aq * |{u,v,(ar * w)}|) by Th27
.= ap * (aq * (ar * |{u,v,w}|)) by Th28
.= 0 by A27 ;
reconsider pf = up, qf = uq, rf = ur as FinSequence of F_Real by EUCLID:24;
A32: ( N * pf = N * (<*pf*> @) & N * qf = N * (<*qf*> @) & N * rf = N * (<*rf*> @) ) by LAPLACE:def 9;
A33: ( len pf = 3 & len qf = 3 & len rf = 3 ) by FINSEQ_3:153;
( N * (<*pf*> @) is Matrix of 3,1,F_Real & N * (<*qf*> @) is Matrix of 3,1,F_Real & N * (<*rf*> @) is Matrix of 3,1,F_Real ) by FINSEQ_3:153, Th74;
then reconsider pt = N * pf, qt = N * qf, rt = N * rf as FinSequence of 1 -tuples_on REAL by A32, Th79;
A34: ( pt = N * (<*pf*> @) & qt = N * (<*qf*> @) & rt = N * (<*rf*> @) ) by LAPLACE:def 9;
A35: width N = 3 by MATRIX_0:23;
width <*pf*> = 3 by A33, Th61;
then A36: len (<*pf*> @) = width <*pf*> by MATRIX_0:29
.= len pf by MATRIX_0:23
.= 3 by FINSEQ_3:153 ;
width <*qf*> = 3 by A33, Th61;
then A37: len (<*qf*> @) = width <*qf*> by MATRIX_0:29
.= len qf by MATRIX_0:23
.= 3 by FINSEQ_3:153 ;
width <*rf*> = 3 by A33, Th61;
then len (<*rf*> @) = width <*rf*> by MATRIX_0:29
.= len rf by MATRIX_0:23
.= 3 by FINSEQ_3:153 ;
then ( len pt = len N & len qt = len N & len rt = len N ) by A35, A37, A36, A34, MATRIX_3:def 4;
then reconsider pm = M2F pt, qm = M2F qt, rm = M2F rt as Element of (TOP-REAL 3) by MATRIX_0:23, Th66;
A38: |{pm,qm,rm}| = 0 by A31, Th78;
( not pm is zero & not qm is zero & not rm is zero ) by A3, A9, A15, Th82;
hence (homography N) . p,(homography N) . q,(homography N) . r are_collinear by A38, Th37, ANPROJ_2:23, A6, A12, A18, A7, A13, A19, A4, A5, A10, A11, A16, A17; :: thesis:

end;