let P1, P2, P3, P4, P5, P6, P7, P8, P9 be Point of (ProjectiveSpace (TOP-REAL 3)); :: thesis: ( P1,P2,P3,P4,P5,P6,P7,P8,P9 are_in_Pascal_configuration implies ( not P7,P2,P5 are_collinear & not P1,P5,P7 are_collinear & not P2,P4,P7 are_collinear & not P2,P5,P9 are_collinear & not P2,P6,P8 are_collinear & not P2,P7,P8 are_collinear & not P2,P7,P9 are_collinear & not P3,P5,P8 are_collinear & not P3,P6,P8 are_collinear & not P5,P7,P8 are_collinear & not P5,P7,P9 are_collinear ) )
assume A1: P1,P2,P3,P4,P5,P6,P7,P8,P9 are_in_Pascal_configuration ; :: thesis: ( not P7,P2,P5 are_collinear & not P1,P5,P7 are_collinear & not P2,P4,P7 are_collinear & not P2,P5,P9 are_collinear & not P2,P6,P8 are_collinear & not P2,P7,P8 are_collinear & not P2,P7,P9 are_collinear & not P3,P5,P8 are_collinear & not P3,P6,P8 are_collinear & not P5,P7,P8 are_collinear & not P5,P7,P9 are_collinear )
assume A2: ( P7,P2,P5 are_collinear or P1,P5,P7 are_collinear or P2,P4,P7 are_collinear or P2,P5,P9 are_collinear or P2,P6,P8 are_collinear or P2,P7,P8 are_collinear or P2,P7,P9 are_collinear or P3,P5,P8 are_collinear or P3,P6,P8 are_collinear or P5,P7,P8 are_collinear or P5,P7,P9 are_collinear ) ; :: thesis: contradiction
( not P1,P2,P4 are_collinear & not P1,P2,P5 are_collinear & not P1,P2,P6 are_collinear & not P1,P3,P4 are_collinear & not P1,P3,P5 are_collinear & not P1,P3,P6 are_collinear & not P2,P3,P4 are_collinear & not P2,P3,P5 are_collinear & not P4,P5,P1 are_collinear & not P4,P5,P2 are_collinear & not P4,P5,P3 are_collinear & not P4,P6,P2 are_collinear & not P4,P6,P3 are_collinear & not P5,P6,P2 are_collinear & P1,P5,P9 are_collinear & P1,P6,P8 are_collinear & P2,P4,P9 are_collinear & P2,P6,P7 are_collinear & P3,P4,P8 are_collinear & P3,P5,P7 are_collinear ) by A1, ANPROJ_8:57, HESSENBE:1;
hence contradiction by A2, ANPROJ_8:57, Th31; :: thesis: verum