for P1, P2, P3, P4, P5, P6, P7, P8, P9 being Point of (ProjectiveSpace (TOP-REAL 3)) st P1,P2,P3,P4,P5,P6,P7,P8,P9 are_in_Pascal_configuration holds
( 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 )