let P1, P2, P3, P4, P5, P6, P7, P8, P9 be Point of (ProjectiveSpace (TOP-REAL 3)); :: thesis: for a, b, c, d, e, f being Real st ( not a = 0 or not b = 0 or not c = 0 or not d = 0 or not e = 0 or not f = 0 ) & {P1,P2,P3,P4,P5,P6} c= conic (a,b,c,d,e,f) & P1,P2,P3 are_collinear & P1,P2,P3,P4,P5,P6,P7,P8,P9 are_in_Pascal_configuration holds
P7,P8,P9 are_collinear
let a, b, c, d, e, f be Real; :: thesis: ( ( not a = 0 or not b = 0 or not c = 0 or not d = 0 or not e = 0 or not f = 0 ) & {P1,P2,P3,P4,P5,P6} c= conic (a,b,c,d,e,f) & P1,P2,P3 are_collinear & P1,P2,P3,P4,P5,P6,P7,P8,P9 are_in_Pascal_configuration implies P7,P8,P9 are_collinear )
assume that
A1: ( not a = 0 or not b = 0 or not c = 0 or not d = 0 or not e = 0 or not f = 0 ) and
A2: {P1,P2,P3,P4,P5,P6} c= conic (a,b,c,d,e,f) and
A3: P1,P2,P3 are_collinear and
A4: P1,P2,P3,P4,P5,P6,P7,P8,P9 are_in_Pascal_configuration ; :: thesis: P7,P8,P9 are_collinear
not P1,P4,P5 are_collinear by A4, COLLSP:8;
then consider N being invertible Matrix of 3,F_Real such that
A5: (homography N) . P1 = Dir100 and
A6: (homography N) . P2 = Dir010 and
A7: (homography N) . P4 = Dir001 and
A8: (homography N) . P5 = Dir111 by A4, ANPROJ_9:30;
consider u3 being Point of (TOP-REAL 3) such that
A9: not u3 is zero and
A10: (homography N) . P3 = Dir u3 by ANPROJ_1:26;
reconsider p31 = u3 . 1, p32 = u3 . 2, p33 = u3 . 3 as Real ;
A11: ( u3 `1 = u3 . 1 & u3 `2 = u3 . 2 & u3 `3 = u3 . 3 ) by EUCLID_5:def 1, EUCLID_5:def 2, EUCLID_5:def 3;
then A12: (homography N) . P3 = Dir |[p31,p32,p33]| by A10, EUCLID_5:3;
consider u6 being Point of (TOP-REAL 3) such that
A13: not u6 is zero and
A14: (homography N) . P6 = Dir u6 by ANPROJ_1:26;
reconsider p61 = u6 . 1, p62 = u6 . 2, p63 = u6 . 3 as Real ;
A15: ( u6 `1 = u6 . 1 & u6 `2 = u6 . 2 & u6 `3 = u6 . 3 ) by EUCLID_5:def 1, EUCLID_5:def 2, EUCLID_5:def 3;
then A16: (homography N) . P6 = Dir |[p61,p62,p63]| by A14, EUCLID_5:3;
A17: ( P1 in {P1,P2,P3,P4,P5,P6} & P2 in {P1,P2,P3,P4,P5,P6} & P3 in {P1,P2,P3,P4,P5,P6} & P4 in {P1,P2,P3,P4,P5,P6} & P5 in {P1,P2,P3,P4,P5,P6} & P6 in {P1,P2,P3,P4,P5,P6} ) by ENUMSET1:def 4;
consider a2, b2, c2, d2, e2, f2 being Real such that
A18: ( not a2 = 0 or not b2 = 0 or not c2 = 0 or not d2 = 0 or not e2 = 0 or not f2 = 0 ) and
A19: (homography N) . P1 in conic (a2,b2,c2,d2,e2,f2) and
A20: (homography N) . P2 in conic (a2,b2,c2,d2,e2,f2) and
A21: (homography N) . P3 in conic (a2,b2,c2,d2,e2,f2) and
A22: (homography N) . P4 in conic (a2,b2,c2,d2,e2,f2) and
A23: (homography N) . P5 in conic (a2,b2,c2,d2,e2,f2) and
A24: (homography N) . P6 in conic (a2,b2,c2,d2,e2,f2) by A17, A2, A1, Th17;
consider P being Point of (ProjectiveSpace (TOP-REAL 3)) such that
A25: Dir |[1,0,0]| = P and
A26: for u being Element of (TOP-REAL 3) st not u is zero & P = Dir u holds
qfconic (a2,b2,c2,d2,e2,f2,u) = 0 by A5, A19;
A27: ( qfconic (a2,b2,c2,d2,e2,f2,|[1,0,0]|) = 0 & qfconic (a2,b2,c2,d2,e2,f2,|[0,1,0]|) = 0 & qfconic (a2,b2,c2,d2,e2,f2,|[0,0,1]|) = 0 & qfconic (a2,b2,c2,d2,e2,f2,|[1,1,1]|) = 0 & qfconic (a2,b2,c2,d2,e2,f2,|[p31,p32,p33]|) = 0 & qfconic (a2,b2,c2,d2,e2,f2,|[p61,p62,p63]|) = 0 )
proof
thus qfconic (a2,b2,c2,d2,e2,f2,|[1,0,0]|) = 0 by A25, A26, ANPROJ_9:10; :: thesis: ( qfconic (a2,b2,c2,d2,e2,f2,|[0,1,0]|) = 0 & qfconic (a2,b2,c2,d2,e2,f2,|[0,0,1]|) = 0 & qfconic (a2,b2,c2,d2,e2,f2,|[1,1,1]|) = 0 & qfconic (a2,b2,c2,d2,e2,f2,|[p31,p32,p33]|) = 0 & qfconic (a2,b2,c2,d2,e2,f2,|[p61,p62,p63]|) = 0 )
consider P being Point of (ProjectiveSpace (TOP-REAL 3)) such that
A28: Dir |[0,1,0]| = P and
A29: for u being Element of (TOP-REAL 3) st not u is zero & P = Dir u holds
qfconic (a2,b2,c2,d2,e2,f2,u) = 0 by A6, A20;
thus qfconic (a2,b2,c2,d2,e2,f2,|[0,1,0]|) = 0 by A28, A29, ANPROJ_9:10; :: thesis: ( qfconic (a2,b2,c2,d2,e2,f2,|[0,0,1]|) = 0 & qfconic (a2,b2,c2,d2,e2,f2,|[1,1,1]|) = 0 & qfconic (a2,b2,c2,d2,e2,f2,|[p31,p32,p33]|) = 0 & qfconic (a2,b2,c2,d2,e2,f2,|[p61,p62,p63]|) = 0 )
consider P being Point of (ProjectiveSpace (TOP-REAL 3)) such that
A30: Dir |[0,0,1]| = P and
A31: for u being Element of (TOP-REAL 3) st not u is zero & P = Dir u holds
qfconic (a2,b2,c2,d2,e2,f2,u) = 0 by A7, A22;
thus qfconic (a2,b2,c2,d2,e2,f2,|[0,0,1]|) = 0 by A30, A31, ANPROJ_9:10; :: thesis: ( qfconic (a2,b2,c2,d2,e2,f2,|[1,1,1]|) = 0 & qfconic (a2,b2,c2,d2,e2,f2,|[p31,p32,p33]|) = 0 & qfconic (a2,b2,c2,d2,e2,f2,|[p61,p62,p63]|) = 0 )
consider P being Point of (ProjectiveSpace (TOP-REAL 3)) such that
A32: Dir |[1,1,1]| = P and
A33: for u being Element of (TOP-REAL 3) st not u is zero & P = Dir u holds
qfconic (a2,b2,c2,d2,e2,f2,u) = 0 by A8, A23;
thus qfconic (a2,b2,c2,d2,e2,f2,|[1,1,1]|) = 0 by A32, A33, ANPROJ_9:10; :: thesis: ( qfconic (a2,b2,c2,d2,e2,f2,|[p31,p32,p33]|) = 0 & qfconic (a2,b2,c2,d2,e2,f2,|[p61,p62,p63]|) = 0 )
consider P being Point of (ProjectiveSpace (TOP-REAL 3)) such that
A34: Dir |[p31,p32,p33]| = P and
A35: for u being Element of (TOP-REAL 3) st not u is zero & P = Dir u holds
qfconic (a2,b2,c2,d2,e2,f2,u) = 0 by A12, A21;
( not |[p31,p32,p33]| is zero & Dir |[p31,p32,p33]| = P ) by A34, A9, A11, EUCLID_5:3;
hence qfconic (a2,b2,c2,d2,e2,f2,|[p31,p32,p33]|) = 0 by A35; :: thesis: qfconic (a2,b2,c2,d2,e2,f2,|[p61,p62,p63]|) = 0
consider P being Point of (ProjectiveSpace (TOP-REAL 3)) such that
A36: Dir |[p61,p62,p63]| = P and
A37: for u being Element of (TOP-REAL 3) st not u is zero & P = Dir u holds
qfconic (a2,b2,c2,d2,e2,f2,u) = 0 by A16, A24;
( not |[p61,p62,p63]| is zero & Dir |[p61,p62,p63]| = P ) by A36, A15, EUCLID_5:3, A13;
hence qfconic (a2,b2,c2,d2,e2,f2,|[p61,p62,p63]|) = 0 by A37; :: thesis: verum
end;
reconsider a2f = a2, b2f = b2, c2f = c2, d2f = d2, e2f = e2, f2f = f2 as Element of F_Real by XREAL_0:def 1;
( qfconic (a2f,b2f,c2f,d2f,e2,f2f,|[1,0,0]|) = 0 & qfconic (a2f,b2f,c2f,d2f,e2f,f2f,|[0,1,0]|) = 0 & qfconic (a2f,b2f,c2f,d2f,e2f,f2f,|[0,0,1]|) = 0 & qfconic (a2f,b2f,c2f,d2f,e2f,f2f,|[1,1,1]|) = 0 & qfconic (a2f,b2f,c2f,d2f,e2f,f2f,|[p31,p32,p33]|) = 0 & qfconic (a2f,b2f,c2f,d2f,e2f,f2f,|[p61,p62,p63]|) = 0 ) by A27;
then A38: ( a2f = 0 & b2f = 0 & c2f = 0 ) by Th18;
then A39: ( a2f = 0 & b2f = 0 & c2f = 0 & (d2f + e2f) + f2f = 0 ) by A27, Th18;
reconsider r1 = d2, r2 = f2 as Real ;
( |[1,0,0]| = <*1,0,0*> & <*0,1,0*> = |[0,1,0]| & <*0,0,1*> = |[0,0,1]| & <*1,1,1*> = |[1,1,1]| & <*p31,p32,p33*> = |[p31,p32,p33]| & <*p61,p62,p63*> = |[p61,p62,p63]| ) ;
then reconsider p1 = <*1,0,0*>, p2 = <*0,1,0*>, p4 = <*0,0,1*>, p5 = <*1,1,1*>, p3 = <*p31,p32,p33*>, p6 = <*p61,p62,p63*> as Point of (TOP-REAL 3) ;
A42: u3 = |[p31,p32,p33]| by EUCLID_5:3, A11;
A43: u6 = |[p61,p62,p63]| by A15, EUCLID_5:3;
A44: ( ( r1 <> 0 or r2 <> 0 ) & qfconic (0,0,0,r1,(- (r1 + r2)),r2,p3) = 0 & qfconic (0,0,0,r1,(- (r1 + r2)),r2,p6) = 0 ) by A39, A27, A18;
A45: ( p1 `1 = 1 & p1 `2 = 0 & p1 `3 = 0 & p2 `1 = 0 & p2 `2 = 1 & p2 `3 = 0 & p3 `1 = p31 & p3 `2 = p32 & p3 `3 = p33 ) by EUCLID_5:2;
A46: ( p3 `1 = p3 . 1 & p3 `2 = p3 . 2 & p3 `3 = p3 . 3 ) by EUCLID_5:def 1, EUCLID_5:def 2, EUCLID_5:def 3;
A47: ( (homography N) . P1 = Dir p1 & (homography N) . P2 = Dir p2 & (homography N) . P3 = Dir p3 ) by A5, A6, A11, A10, EUCLID_5:3;
|{p1,p2,p3}| = 0
proof
consider u, v, w being Element of (TOP-REAL 3) such that
A48: (homography N) . P1 = Dir u and
A49: (homography N) . P2 = Dir v and
A50: (homography N) . P3 = Dir w and
A51: not u is zero and
A52: not v is zero and
A53: not w is zero and
A54: u,v,w are_LinDep by A3, ANPROJ_8:102, ANPROJ_2:23;
A55: [(Dir u),(Dir v),(Dir w)] in the Collinearity of (ProjectiveSpace (TOP-REAL 3)) by A51, A52, A53, A54, ANPROJ_1:25;
p1,p2,p3 are_LinDep by A5, A6, A10, ANPROJ_9:10, A42, A9, A48, A49, A50, A55, ANPROJ_1:25;
hence |{p1,p2,p3}| = 0 by ANPROJ_8:43; :: thesis: verum
end;
then A56: 0 = ((((((1 * (p2 `2)) * (p3 `3)) - ((0 * (p2 `2)) * (p3 `1))) - ((1 * (p2 `3)) * (p3 `2))) + ((0 * (p2 `3)) * (p3 `1))) - ((0 * (p2 `1)) * (p3 `3))) + ((0 * (p2 `1)) * (p3 `2)) by A45, ANPROJ_8:27
.= p3 `3 by A45 ;
A57: ( p31 <> 0 & p32 <> 0 )
proof
assume ( p31 = 0 or p32 = 0 ) ; :: thesis: contradiction
per cases then ( p31 = 0 or p32 = 0 ) ;
suppose p31 = 0 ; :: thesis: contradiction
then A58: p3 = |[(p32 * 0),(p32 * 1),(p32 * 0)]| by A56, EUCLID_5:2
.= p32 * |[0,1,0]| by EUCLID_5:8 ;
now :: thesis: ( are_Prop p3,|[0,1,0]| & not p3 is zero & not |[0,1,0]| is zero )
p32 <> 0
proof
assume p32 = 0 ; :: thesis: contradiction
then p3 = |[(0 * 0),(0 * 1),(0 * 0)]| by A58, EUCLID_5:8
.= 0. (TOP-REAL 3) by EUCLID_5:4 ;
hence contradiction by A11, EUCLID_5:3, A9; :: thesis: verum
end;
hence are_Prop p3,|[0,1,0]| by A58, ANPROJ_1:1; :: thesis: ( not p3 is zero & not |[0,1,0]| is zero )
thus not p3 is zero by A11, EUCLID_5:3, A9; :: thesis: not |[0,1,0]| is zero
thus not |[0,1,0]| is zero by ANPROJ_9:11; :: thesis: verum
end;
then (homography N) . P3 = (homography N) . P2 by A47, ANPROJ_1:22;
then P3 = P2 by ANPROJ_9:16;
hence contradiction by A4, ANPROJ_2:def 7; :: thesis: verum
end;
suppose p32 = 0 ; :: thesis: contradiction
then A59: p3 = |[(p31 * 1),(p31 * 0),(p31 * 0)]| by A56, EUCLID_5:2
.= p31 * |[1,0,0]| by EUCLID_5:8 ;
now :: thesis: ( are_Prop p3,|[1,0,0]| & not p3 is zero & not |[1,0,0]| is zero )
p31 <> 0
proof
assume p31 = 0 ; :: thesis: contradiction
then p3 = |[(0 * 1),(0 * 0),(0 * 0)]| by A59, EUCLID_5:8
.= 0. (TOP-REAL 3) by EUCLID_5:4 ;
hence contradiction by EUCLID_5:3, A11, A9; :: thesis: verum
end;
hence are_Prop p3,|[1,0,0]| by A59, ANPROJ_1:1; :: thesis: ( not p3 is zero & not |[1,0,0]| is zero )
thus not p3 is zero by EUCLID_5:3, A11, A9; :: thesis: not |[1,0,0]| is zero
thus not |[1,0,0]| is zero by ANPROJ_9:11; :: thesis: verum
end;
then Dir p3 = Dir100 by ANPROJ_1:22;
then P3 = P1 by A47, ANPROJ_9:16;
hence contradiction by ANPROJ_2:def 7, A4; :: thesis: verum
end;
end;
end;
now :: thesis: ( (r2 * (p6 . 3)) * ((p6 . 1) - (p6 . 2)) = 0 & r2 <> 0 )
A60: r1 = 0
proof
assume r1 <> 0 ; :: thesis: contradiction
then r1 * p31 <> 0 by A57, XCMPLX_1:6;
hence contradiction by A57, XCMPLX_1:6, A38, A27, A46, A56, A45; :: thesis: verum
end;
hence (r2 * (p6 . 3)) * ((p6 . 1) - (p6 . 2)) = 0 by A44; :: thesis: r2 <> 0
thus r2 <> 0 :: thesis: verum
proof
assume A61: r2 = 0 ; :: thesis: contradiction
A62: ( a2f = 0 & b2f = 0 & c2f = 0 & (d2f + e2f) + f2f = 0 ) by A38, A27, Th18;
thus contradiction by A18, A62, A60, A61; :: thesis: verum
end;
end;
then ( r2 <> 0 & ( r2 * (p6 . 3) = 0 or (p6 . 1) - (p6 . 2) = 0 ) ) by XCMPLX_1:6;
per cases then ( p6 . 3 = 0 or p6 . 1 = p6 . 2 ) by XCMPLX_1:6;
suppose p6 . 3 = 0 ; :: thesis: P7,P8,P9 are_collinear
then A63: p6 `3 = 0 by EUCLID_5:def 3;
A64: p6 = |[(p61 + 0),(0 + p62),(0 + 0)]| by A63, EUCLID_5:2
.= |[(p61 * 1),(p61 * 0),(p61 * 0)]| + |[(p62 * 0),(p62 * 1),(p62 * 0)]| by EUCLID_5:6
.= (p61 * |[1,0,0]|) + |[(p62 * 0),(p62 * 1),(p62 * 0)]| by EUCLID_5:8
.= (p61 * |[1,0,0]|) + (p62 * |[0,1,0]|) by EUCLID_5:8 ;
per cases ( ( p61 = 0 & p62 = 0 ) or ( p61 <> 0 & p62 = 0 ) or ( p61 = 0 & p62 <> 0 ) or ( p61 <> 0 & p62 <> 0 ) ) ;
suppose A65: ( p61 <> 0 & p62 = 0 ) ; :: thesis: P7,P8,P9 are_collinear
now :: thesis: ( are_Prop p6,|[1,0,0]| & not p6 is zero & not |[1,0,0]| is zero )
p6 = |[(p61 * 1),(p61 * 0),(p61 * 0)]| by A63, EUCLID_5:2, A65
.= p61 * |[1,0,0]| by EUCLID_5:8 ;
hence are_Prop p6,|[1,0,0]| by A65, ANPROJ_1:1; :: thesis: ( not p6 is zero & not |[1,0,0]| is zero )
thus not p6 is zero by A15, EUCLID_5:3, A13; :: thesis: not |[1,0,0]| is zero
thus not |[1,0,0]| is zero by ANPROJ_9:11; :: thesis: verum
end;
then Dir p6 = Dir100 by ANPROJ_1:22;
then P1 = P6 by ANPROJ_9:16, A5, A14, A43;
hence P7,P8,P9 are_collinear by A4, ANPROJ_2:def 7; :: thesis: verum
end;
suppose A66: ( p61 = 0 & p62 <> 0 ) ; :: thesis: P7,P8,P9 are_collinear
now :: thesis: ( are_Prop p6,|[0,1,0]| & not p6 is zero & not |[0,1,0]| is zero )
p6 = |[(p62 * 0),(p62 * 1),(p62 * 0)]| by A63, EUCLID_5:2, A66
.= p62 * |[0,1,0]| by EUCLID_5:8 ;
hence are_Prop p6,|[0,1,0]| by A66, ANPROJ_1:1; :: thesis: ( not p6 is zero & not |[0,1,0]| is zero )
thus not p6 is zero by A15, EUCLID_5:3, A13; :: thesis: not |[0,1,0]| is zero
thus not |[0,1,0]| is zero by ANPROJ_9:11; :: thesis: verum
end;
then Dir p6 = Dir010 by ANPROJ_1:22;
then P2 = P6 by ANPROJ_9:16, A6, A14, A43;
hence P7,P8,P9 are_collinear by A4, ANPROJ_2:def 7; :: thesis: verum
end;
suppose ( p61 <> 0 & p62 <> 0 ) ; :: thesis: P7,P8,P9 are_collinear
now :: thesis: ( |[1,0,0]|,|[0,1,0]|,p6 are_LinDep & not |[1,0,0]| is zero & not |[0,1,0]| is zero & not p6 is zero )
now :: thesis: ( p6 = (p61 * |[1,0,0]|) + (p62 * |[0,1,0]|) & not |[1,0,0]| is zero & not |[0,1,0]| is zero & not are_Prop |[1,0,0]|,|[0,1,0]| )
thus p6 = (p61 * |[1,0,0]|) + (p62 * |[0,1,0]|) by A64; :: thesis: ( not |[1,0,0]| is zero & not |[0,1,0]| is zero & not are_Prop |[1,0,0]|,|[0,1,0]| )
thus not |[1,0,0]| is zero by ANPROJ_9:11; :: thesis: ( not |[0,1,0]| is zero & not are_Prop |[1,0,0]|,|[0,1,0]| )
thus not |[0,1,0]| is zero by ANPROJ_9:11; :: thesis: not are_Prop |[1,0,0]|,|[0,1,0]|
thus not are_Prop |[1,0,0]|,|[0,1,0]| :: thesis: verum
proof
assume are_Prop |[1,0,0]|,|[0,1,0]| ; :: thesis: contradiction
then consider a being Real such that
a <> 0 and
A67: |[1,0,0]| = a * |[0,1,0]| by ANPROJ_1:1;
|[1,0,0]| = |[(a * 0),(a * 1),(a * 0)]| by A67, EUCLID_5:8
.= |[0,a,0]| ;
hence contradiction by FINSEQ_1:78; :: thesis: verum
end;
end;
hence |[1,0,0]|,|[0,1,0]|,p6 are_LinDep by ANPROJ_1:6; :: thesis: ( not |[1,0,0]| is zero & not |[0,1,0]| is zero & not p6 is zero )
thus not |[1,0,0]| is zero by ANPROJ_9:11; :: thesis: ( not |[0,1,0]| is zero & not p6 is zero )
thus not |[0,1,0]| is zero by ANPROJ_9:11; :: thesis: not p6 is zero
thus not p6 is zero by A15, EUCLID_5:3, A13; :: thesis: verum
end;
then [Dir100,Dir010,(Dir p6)] in the Collinearity of (ProjectiveSpace (TOP-REAL 3)) by ANPROJ_1:25;
hence P7,P8,P9 are_collinear by A4, A5, A6, A14, A43, COLLSP:def 2, ANPROJ_8:102; :: thesis: verum
end;
end;
end;
suppose A68: p6 . 1 = p6 . 2 ; :: thesis: P7,P8,P9 are_collinear
A69: p61 = p6 `1 by EUCLID_5:2
.= p6 . 2 by A68, EUCLID_5:def 1
.= p6 `2 by EUCLID_5:def 2
.= p62 by EUCLID_5:2 ;
now :: thesis: ( not p4 is zero & not p5 is zero & not p6 is zero & |[0,0,1]|,|[1,1,1]|,p6 are_LinDep )
thus not p4 is zero by ANPROJ_9:11; :: thesis: ( not p5 is zero & not p6 is zero & |[0,0,1]|,|[1,1,1]|,p6 are_LinDep )
thus not p5 is zero by ANPROJ_9:11; :: thesis: ( not p6 is zero & |[0,0,1]|,|[1,1,1]|,p6 are_LinDep )
thus not p6 is zero by A13, A15, EUCLID_5:3; :: thesis: |[0,0,1]|,|[1,1,1]|,p6 are_LinDep
|{p4,p5,p6}| = 0
proof
( p6 `1 = p61 & p6 `2 = p61 & p4 `1 = 0 & p4 `2 = 0 & p4 `3 = 1 & p5 `1 = 1 & p5 `2 = 1 & p5 `3 = 1 & |{p4,p5,p6}| = (((((((p4 `1) * (p5 `2)) * (p6 `3)) - (((p4 `3) * (p5 `2)) * (p6 `1))) - (((p4 `1) * (p5 `3)) * (p6 `2))) + (((p4 `2) * (p5 `3)) * (p6 `1))) - (((p4 `2) * (p5 `1)) * (p6 `3))) + (((p4 `3) * (p5 `1)) * (p6 `2)) ) by EUCLID_5:2, A69, ANPROJ_8:27;
hence |{p4,p5,p6}| = 0 ; :: thesis: verum
end;
hence |[0,0,1]|,|[1,1,1]|,p6 are_LinDep by ANPROJ_8:43; :: thesis: verum
end;
then A70: [Dir001,Dir111,(Dir p6)] in the Collinearity of (ProjectiveSpace (TOP-REAL 3)) by ANPROJ_1:25;
reconsider p1 = P1, p2 = P2, p3 = P3, q1 = P4, q2 = P5, q3 = P6, r1 = P7, r2 = P8, r3 = P9 as Element of (ProjectiveSpace (TOP-REAL 3)) ;
( p2 <> p3 & p1 <> p3 & q2 <> q3 & q1 <> q2 & q1 <> q3 & not p1,p2,q1 are_collinear & p1,p2,p3 are_collinear & q1,q2,q3 are_collinear & p1,q2,r3 are_collinear & q1,p2,r3 are_collinear & p1,q3,r2 are_collinear & p3,q1,r2 are_collinear & p2,q3,r1 are_collinear & p3,q2,r1 are_collinear ) by COLLSP:2, A3, A4, A70, A7, A8, A14, A43, COLLSP:def 2, ANPROJ_2:24, ANPROJ_8:102;
hence P7,P8,P9 are_collinear by ANPROJ_8:57, HESSENBE:16; :: thesis: verum
end;
end;