:: Pascal's Theorem in Real Projective Plane
:: by Roland Coghetto
::
:: Received June 27, 2017
:: Copyright (c) 2017-2021 Association of Mizar Users

theorem Th01: :: PASCAL:1

for p, q, r being Point of (TOP-REAL 3) holds
( |{p,q,r}| = |{r,p,q}| & |{p,q,r}| = |{q,r,p}| )

proof end;

theorem Th02: :: PASCAL:2

for K being Field
for a, b, c, d, e, f, g, h, i, a1, b1, c1, d1, e1, f1, g1, h1, i1 being Element of K st <*<*a,b,c*>,<*d,e,f*>,<*g,h,i*>*> = <*<*a1,b1,c1*>,<*d1,e1,f1*>,<*g1,h1,i1*>*> holds
( a = a1 & b = b1 & c = c1 & d = d1 & e = e1 & f = f1 & g = g1 & h = h1 & i = i1 )

proof end;

theorem Th03: :: PASCAL:3

for K being Field
for M being Matrix of 3,K ex a, b, c, d, e, f, g, h, i being Element of K st M = <*<*a,b,c*>,<*d,e,f*>,<*g,h,i*>*>

proof end;

theorem Th04: :: PASCAL:4

for K being Field
for a, b, c, d, e, f, g, h, i being Element of K
for M being Matrix of 3,K st M = <*<*a,b,c*>,<*d,e,f*>,<*g,h,i*>*> holds
( a = M * (1,1) & b = M * (1,2) & c = M * (1,3) & d = M * (2,1) & e = M * (2,2) & f = M * (2,3) & g = M * (3,1) & h = M * (3,2) & i = M * (3,3) )

proof end;

theorem Th05: :: PASCAL:5

for K being Field
for a, b, c, d, e, f, g, h, i being Element of K
for M being Matrix of 3,K st M = <*<*a,b,c*>,<*d,e,f*>,<*g,h,i*>*> holds
M @ = <*<*a,d,g*>,<*b,e,h*>,<*c,f,i*>*>

proof end;

theorem Th06: :: PASCAL:6

for K being Field
for a, b, c, d, e, f, g, h, i being Element of K
for M being Matrix of 3,K st M = <*<*a,b,c*>,<*d,e,f*>,<*g,h,i*>*> & M is symmetric holds
( b = d & c = g & h = f )

proof end;

theorem Th07: :: PASCAL:7

for M, N being Matrix of 3,F_Real st N is symmetric holds
((M @) * N) * M is symmetric

proof end;

theorem Th08: :: PASCAL:8

for M being Matrix of 3,F_Real
for a, b, c, d, e, f, g, h, i, x, y, z being Element of F_Real
for v being Element of (TOP-REAL 3)
for uf being FinSequence of F_Real
for p being FinSequence of 1 -tuples_on REAL st p = M * uf & v = M2F p & M = <*<*a,b,c*>,<*d,e,f*>,<*g,h,i*>*> & uf = <*x,y,z*> holds
( p = <*<*(((a * x) + (b * y)) + (c * z))*>,<*(((d * x) + (e * y)) + (f * z))*>,<*(((g * x) + (h * y)) + (i * z))*>*> & v = <*(((a * x) + (b * y)) + (c * z)),(((d * x) + (e * y)) + (f * z)),(((g * x) + (h * y)) + (i * z))*> )

proof end;

Lm01: for p being FinSequence of REAL
for N1, M, N2 being Matrix of 3,REAL st len p = 3 holds
((N1 * M) * N2) * p = N1 * (M * (N2 * p))

proof end;

Lm02: for p being FinSequence of REAL
for N, M being Matrix of 3,REAL st len p = 3 holds
|((N * p),(M * (N * p)))| = |(p,((((N @) * M) * N) * p))|

proof end;

Lm03: for NR, M being Matrix of 3,REAL holds ((MXF2MXR ((MXR2MXF (NR @)) ~)) * M) * (MXF2MXR ((MXR2MXF NR) ~)) is Matrix of 3,REAL

proof end;

Lm04: for n being Nat
for A, B, C, D, E being Matrix of n,REAL holds (A * ((B * C) * D)) * E = ((A * B) * C) * (D * E)

proof end;

Lm05: for n being Nat
for A, B being Matrix of n,F_Real holds MXF2MXR (A * B) = (MXF2MXR A) * (MXF2MXR B)

proof end;

Lm06: for A being Matrix of REAL holds MXF2MXR (MXR2MXF A) = A

proof end;

Lm07: for n being Nat
for A, B being Matrix of n,REAL holds MXR2MXF (A * B) = (MXR2MXF A) * (MXR2MXF B)

proof end;

Lm08: for N being invertible Matrix of 3,F_Real
for NR being Matrix of 3,REAL st NR = MXF2MXR N holds
NR * (MXF2MXR ((MXR2MXF NR) ~)) = 1_Rmatrix 3

proof end;

Lm09: for N being invertible Matrix of 3,F_Real
for NR being Matrix of 3,REAL st NR = MXF2MXR N holds
(NR @) * (MXF2MXR ((MXR2MXF (NR @)) ~)) = 1_Rmatrix 3

proof end;

Lm10: for N being invertible Matrix of 3,F_Real
for NR being Matrix of 3,REAL st NR = MXF2MXR N holds
(MXF2MXR ((MXR2MXF NR) ~)) * NR = 1_Rmatrix 3

proof end;

Lm11: for N being invertible Matrix of 3,F_Real
for NR being Matrix of 3,REAL st NR = MXF2MXR N holds
(MXF2MXR ((MXR2MXF (NR @)) ~)) * (NR @) = 1_Rmatrix 3

proof end;

Lm12: for N being invertible Matrix of 3,F_Real
for NR being Matrix of 3,REAL st NR = MXF2MXR N holds
NR @ is invertible

proof end;

Lm13: for N being invertible Matrix of 3,F_Real
for NR, M, M2 being Matrix of 3,REAL st NR = MXF2MXR N & M2 = ((MXF2MXR ((MXR2MXF (NR @)) ~)) * M) * (MXF2MXR ((MXR2MXF NR) ~)) holds
((NR @) * M2) * NR = M

proof end;

Lm14: for n being Nat
for N being invertible Matrix of n,F_Real
for M being Matrix of n,REAL st M = MXF2MXR N holds
M is invertible

proof end;

Lm15: for n being Nat
for N being Matrix of n,F_Real
for M being Matrix of n,REAL st M is invertible & N = MXR2MXF M holds
N is invertible

proof end;

theorem Th09: :: PASCAL:9

for p being FinSequence of REAL
for M being Matrix of 3,REAL
for a, b, c, d, e, f, g, h, i, p1, p2, p3 being Element of REAL st M = <*<*a,b,c*>,<*d,e,f*>,<*g,h,i*>*> & p = <*p1,p2,p3*> holds
M * p = <*(((a * p1) + (b * p2)) + (c * p3)),(((d * p1) + (e * p2)) + (f * p3)),(((g * p1) + (h * p2)) + (i * p3))*>

proof end;

Lm16: for p being FinSequence of REAL
for M being Matrix of 3,REAL st p = 0. (TOP-REAL 3) holds
M * p = p

proof end;

Lm17: <*<*0,0,0*>,<*0,0,0*>,<*0,0,0*>*> = 0. (F_Real,3,3)

proof end;

Lm18: <*<*0,0,0*>,<*0,0,0*>,<*0,0,0*>*> = 0_Rmatrix 3

proof end;

Lm19: for n being Nat
for K being Field
for M being Matrix of n,K st n > 0 holds
M * (0. (K,n,n)) = 0. (K,n,n)

proof end;

Lm20: for M being Matrix of 3,REAL holds
( M * (0_Rmatrix 3) = 0_Rmatrix 3 & (0_Rmatrix 3) * M = 0_Rmatrix 3 )

proof end;

definition

let a, b, c, d, e, f be Real;
let u be Element of (TOP-REAL 3);

func qfconic (a,b,c,d,e,f,u) -> Real equals :: PASCAL:def 1
((((((a * (u . 1)) * (u . 1)) + ((b * (u . 2)) * (u . 2))) + ((c * (u . 3)) * (u . 3))) + ((d * (u . 1)) * (u . 2))) + ((e * (u . 1)) * (u . 3))) + ((f * (u . 2)) * (u . 3));

coherence
((((((a * (u . 1)) * (u . 1)) + ((b * (u . 2)) * (u . 2))) + ((c * (u . 3)) * (u . 3))) + ((d * (u . 1)) * (u . 2))) + ((e * (u . 1)) * (u . 3))) + ((f * (u . 2)) * (u . 3)) is Real ;

end;

:: deftheorem defines qfconic PASCAL:def 1 :
for a, b, c, d, e, f being Real
for u being Element of (TOP-REAL 3) holds qfconic (a,b,c,d,e,f,u) = ((((((a * (u . 1)) * (u . 1)) + ((b * (u . 2)) * (u . 2))) + ((c * (u . 3)) * (u . 3))) + ((d * (u . 1)) * (u . 2))) + ((e * (u . 1)) * (u . 3))) + ((f * (u . 2)) * (u . 3));

definition

let a, b, c, d, e, f be Real;

func conic (a,b,c,d,e,f) -> Subset of (ProjectiveSpace (TOP-REAL 3)) equals :: PASCAL:def 2
{ P where P is Point of (ProjectiveSpace (TOP-REAL 3)) : for u being Element of (TOP-REAL 3) st not u is zero & P = Dir u holds
qfconic (a,b,c,d,e,f,u) = 0 } ;

coherence
{ P where P is Point of (ProjectiveSpace (TOP-REAL 3)) : for u being Element of (TOP-REAL 3) st not u is zero & P = Dir u holds
qfconic (a,b,c,d,e,f,u) = 0 } is Subset of (ProjectiveSpace (TOP-REAL 3))

proof end;

end;

:: deftheorem defines conic PASCAL:def 2 :
for a, b, c, d, e, f being Real holds conic (a,b,c,d,e,f) = { P where P is Point of (ProjectiveSpace (TOP-REAL 3)) : for u being Element of (TOP-REAL 3) st not u is zero & P = Dir u holds
qfconic (a,b,c,d,e,f,u) = 0 } ;

theorem Th10: :: PASCAL:10

for a, b, c, d, e, f being Real
for u1, u2 being non zero Element of (TOP-REAL 3) st Dir u1 = Dir u2 & qfconic (a,b,c,d,e,f,u1) = 0 holds
qfconic (a,b,c,d,e,f,u2) = 0

proof end;

theorem Th11: :: PASCAL:11

for a, b, c, d, e, f being Real
for u being non zero Element of (TOP-REAL 3)
for P being Element of (ProjectiveSpace (TOP-REAL 3)) st P = Dir u & qfconic (a,b,c,d,e,f,u) = 0 holds
P in conic (a,b,c,d,e,f)

proof end;

definition

let a, b, c, d, e, f be Real;

func symmetric_3 (a,b,c,d,e,f) -> Matrix of 3,F_Real equals :: PASCAL:def 3
<*<*a,d,e*>,<*d,b,f*>,<*e,f,c*>*>;

coherence
<*<*a,d,e*>,<*d,b,f*>,<*e,f,c*>*> is Matrix of 3,F_Real

proof end;

end;

:: deftheorem defines symmetric_3 PASCAL:def 3 :
for a, b, c, d, e, f being Real holds symmetric_3 (a,b,c,d,e,f) = <*<*a,d,e*>,<*d,b,f*>,<*e,f,c*>*>;

theorem Th12: :: PASCAL:12

for a, b, c, d, e, f being Real holds symmetric_3 (a,b,c,d,e,f) is symmetric

proof end;

theorem Th13: :: PASCAL:13

for p being FinSequence of REAL
for a, b, c, d, e, f being Real
for u being Point of (TOP-REAL 3)
for M being Matrix of 3,REAL st p = u & M = symmetric_3 (a,b,c,d,e,f) holds
SumAll (QuadraticForm (p,M,p)) = qfconic (a,b,c,(2 * d),(2 * e),(2 * f),u)

proof end;

theorem Th14: :: PASCAL:14

for N being invertible Matrix of 3,F_Real
for NR, M1, M2 being Matrix of 3,REAL
for a, b, c, d, e, f being Real st NR = MXF2MXR N & M1 = symmetric_3 (a,b,c,(d / 2),(f / 2),(e / 2)) & M2 = ((MXF2MXR ((MXR2MXF (NR @)) ~)) * M1) * (MXF2MXR ((MXR2MXF NR) ~)) holds
MXR2MXF M2 is symmetric

proof end;

theorem Th15: :: PASCAL:15

for a1, a2, a3, a4, a5, a6, b1, b2, b3, b4, b5, b6 being Real st symmetric_3 (a1,a2,a3,a4,a5,a6) = symmetric_3 (b1,b2,b3,b4,b5,b6) holds
( a1 = b1 & a2 = b2 & a3 = b3 & a4 = b4 & a5 = b5 & a6 = b6 )

proof end;

theorem Th16: :: PASCAL:16

for a, b, c, d, e, f being Real
for P being Point of (ProjectiveSpace (TOP-REAL 3))
for N being invertible Matrix of 3,F_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 ) & P in conic (a,b,c,d,e,f) holds
for fa, fb, fc, fd, fe, fi, ff being Real
for M1, M2, NR being Matrix of 3,REAL st M1 = symmetric_3 (a,b,c,(d / 2),(e / 2),(f / 2)) & NR = MXF2MXR N & M2 = ((MXF2MXR ((MXR2MXF (NR @)) ~)) * M1) * (MXF2MXR ((MXR2MXF NR) ~)) & M2 = symmetric_3 (fa,fe,fi,fb,fc,ff) holds
( ( not fa = 0 or not fe = 0 or not fi = 0 or not fb = 0 or not ff = 0 or not fc = 0 ) & (homography N) . P in conic (fa,fe,fi,(2 * fb),(2 * fc),(2 * ff)) )

proof end;

theorem Th17: :: PASCAL:17

for a, b, c, d, e, f being Real
for P1, P2, P3, P4, P5, P6 being Point of (ProjectiveSpace (TOP-REAL 3))
for N being invertible Matrix of 3,F_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 in conic (a,b,c,d,e,f) & P2 in conic (a,b,c,d,e,f) & P3 in conic (a,b,c,d,e,f) & P4 in conic (a,b,c,d,e,f) & P5 in conic (a,b,c,d,e,f) & P6 in conic (a,b,c,d,e,f) holds
ex a2, b2, c2, d2, e2, f2 being Real st
( ( not a2 = 0 or not b2 = 0 or not c2 = 0 or not d2 = 0 or not e2 = 0 or not f2 = 0 ) & (homography N) . P1 in conic (a2,b2,c2,d2,e2,f2) & (homography N) . P2 in conic (a2,b2,c2,d2,e2,f2) & (homography N) . P3 in conic (a2,b2,c2,d2,e2,f2) & (homography N) . P4 in conic (a2,b2,c2,d2,e2,f2) & (homography N) . P5 in conic (a2,b2,c2,d2,e2,f2) & (homography N) . P6 in conic (a2,b2,c2,d2,e2,f2) )

proof end;

theorem Th18: :: PASCAL:18

for a, b, c, d, e, f being Element of F_Real holds
( ( qfconic (a,b,c,d,e,f,|[1,0,0]|) = 0 implies a = 0 ) & ( qfconic (a,b,c,d,e,f,|[0,1,0]|) = 0 implies b = 0 ) & ( qfconic (a,b,c,d,e,f,|[0,0,1]|) = 0 implies c = 0 ) & ( qfconic (0,0,0,d,e,f,|[1,1,1]|) = 0 implies (d + e) + f = 0 ) )

proof end;

Lm21: for a, b, c, d, e, f, g, h, i being Element of F_Real
for M being Matrix of 3,F_Real st a = 1 & b = 0 & c = 0 & d = 0 & e = 1 & f = 0 & M = <*<*a,b,c*>,<*d,e,f*>,<*g,h,i*>*> holds
Det M = i

proof end;

Lm22: for r1, r2, d, e, f, g, h, i being Real st ( r1 <> 0 or r2 <> 0 ) & ((r1 * d) * e) + ((r2 * d) * f) = ((r1 + r2) * e) * f & ((r1 * g) * h) + ((r2 * g) * i) = ((r1 + r2) * h) * i holds
((f * h) * (g - i)) * (d - e) = ((i * e) * (d - f)) * (g - h)

proof end;

Lm23: for a, b, c, d, e, f, g, h, i being Element of F_Real
for M being Matrix of 3,F_Real st a = 1 & b = 0 & c = 0 & d = 0 & e = 0 & f = 1 & M = <*<*a,b,c*>,<*d,e,f*>,<*g,h,i*>*> holds
Det M = - h

proof end;

Lm24: for a, b, c, d, e, f, g, h, i being Element of F_Real
for M being Matrix of 3,F_Real st a = 0 & b = 1 & c = 0 & d = 1 & e = 1 & f = 1 & M = <*<*a,b,c*>,<*d,e,f*>,<*g,h,i*>*> holds
Det M = g - i

proof end;

Lm25: for a, b, c, d, e, f, g, h, i being Element of F_Real
for M being Matrix of 3,F_Real st a = 0 & b = 0 & c = 1 & d = 1 & e = 1 & f = 1 & M = <*<*a,b,c*>,<*d,e,f*>,<*g,h,i*>*> holds
Det M = h - g

proof end;

Lm26: for a, b, c, d, e, f, g, h, i being Element of F_Real
for M being Matrix of 3,F_Real st a = 1 & b = 0 & c = 0 & d = 0 & e = 1 & f = 0 & M = <*<*a,b,c*>,<*d,e,f*>,<*g,h,i*>*> holds
Det M = i

proof end;

Lm27: for a, b, c, d, e, f, g, h, i being Element of F_Real
for M being Matrix of 3,F_Real st a = 1 & b = 0 & c = 0 & d = 0 & e = 0 & f = 1 & M = <*<*a,b,c*>,<*d,e,f*>,<*g,h,i*>*> holds
Det M = - h

proof end;

Lm28: for a, b, c, d, e, f, g, h, i being Element of F_Real
for M being Matrix of 3,F_Real st a = 0 & b = 1 & c = 0 & d = 1 & e = 1 & f = 1 & M = <*<*a,b,c*>,<*d,e,f*>,<*g,h,i*>*> holds
Det M = g - i

proof end;

Lm29: for a, b, c, d, e, f, g, h, i being Element of F_Real
for M being Matrix of 3,F_Real st a = 0 & b = 0 & c = 1 & d = 1 & e = 1 & f = 1 & M = <*<*a,b,c*>,<*d,e,f*>,<*g,h,i*>*> holds
Det M = h - g

proof end;

Lm30: for e1, e2, e3, f1, f2, f3 being Element of F_Real
for MABE, MACF, MBDF, MCDE being Matrix of 3,F_Real st MABE = <*<*1,0,0*>,<*0,1,0*>,<*e1,e2,e3*>*> & MACF = <*<*1,0,0*>,<*0,0,1*>,<*f1,f2,f3*>*> & MBDF = <*<*0,1,0*>,<*1,1,1*>,<*f1,f2,f3*>*> & MCDE = <*<*0,0,1*>,<*1,1,1*>,<*e1,e2,e3*>*> holds
(((Det MABE) * (Det MACF)) * (Det MBDF)) * (Det MCDE) = ((e3 * f2) * (f1 - f3)) * (e1 - e2)

proof end;

Lm31: for e1, e2, e3, f1, f2, f3 being Element of F_Real
for MABF, MACE, MBDE, MCDF being Matrix of 3,F_Real st MABF = <*<*1,0,0*>,<*0,1,0*>,<*f1,f2,f3*>*> & MACE = <*<*1,0,0*>,<*0,0,1*>,<*e1,e2,e3*>*> & MBDE = <*<*0,1,0*>,<*1,1,1*>,<*e1,e2,e3*>*> & MCDF = <*<*0,0,1*>,<*1,1,1*>,<*f1,f2,f3*>*> holds
(((Det MABF) * (Det MACE)) * (Det MBDE)) * (Det MCDF) = ((f3 * e2) * (e1 - e3)) * (f1 - f2)

proof end;

theorem Th19: :: PASCAL:19

for e1, e2, e3, f1, f2, f3 being Element of F_Real
for MABF, MABE, MACF, MBDF, MCDE, MACE, MBDE, MCDF being Matrix of 3,F_Real
for r1, r2 being Real st MABE = <*<*1,0,0*>,<*0,1,0*>,<*e1,e2,e3*>*> & MACF = <*<*1,0,0*>,<*0,0,1*>,<*f1,f2,f3*>*> & MBDF = <*<*0,1,0*>,<*1,1,1*>,<*f1,f2,f3*>*> & MCDE = <*<*0,0,1*>,<*1,1,1*>,<*e1,e2,e3*>*> & MABF = <*<*1,0,0*>,<*0,1,0*>,<*f1,f2,f3*>*> & MACE = <*<*1,0,0*>,<*0,0,1*>,<*e1,e2,e3*>*> & MBDE = <*<*0,1,0*>,<*1,1,1*>,<*e1,e2,e3*>*> & MCDF = <*<*0,0,1*>,<*1,1,1*>,<*f1,f2,f3*>*> & ( r1 <> 0 or r2 <> 0 ) & ((r1 * e1) * e2) + ((r2 * e1) * e3) = ((r1 + r2) * e2) * e3 & ((r1 * f1) * f2) + ((r2 * f1) * f3) = ((r1 + r2) * f2) * f3 holds
(((Det MABE) * (Det MACF)) * (Det MBDF)) * (Det MCDE) = (((Det MABF) * (Det MACE)) * (Det MBDE)) * (Det MCDF)

proof end;

theorem Th20: :: PASCAL:20

for MABF, MABE, MACF, MBDF, MCDE, MACE, MBDE, MCDF being Matrix of 3,F_Real
for p1, p2, p3, p4, p5, p6 being Point of (TOP-REAL 3) st MABE = <*p1,p2,p5*> & MACF = <*p1,p3,p6*> & MBDF = <*p2,p4,p6*> & MCDE = <*p3,p4,p5*> & MABF = <*p1,p2,p6*> & MACE = <*p1,p3,p5*> & MBDE = <*p2,p4,p5*> & MCDF = <*p3,p4,p6*> holds
( Det MABE = |{p1,p2,p5}| & Det MACF = |{p1,p3,p6}| & Det MBDF = |{p2,p4,p6}| & Det MCDE = |{p3,p4,p5}| & Det MABF = |{p1,p2,p6}| & Det MACE = |{p1,p3,p5}| & Det MBDE = |{p2,p4,p5}| & Det MCDF = |{p3,p4,p6}| )

proof end;

theorem Th21: :: PASCAL:21

for p1, p2, p5, p7, p9 being Point of (TOP-REAL 3) st |{p1,p5,p9}| = 0 holds
|{p1,p5,p7}| * |{p2,p5,p9}| = - (|{p1,p2,p5}| * |{p5,p9,p7}|)

proof end;

theorem Th22: :: PASCAL:22

for p1, p2, p3, p6, p8 being Point of (TOP-REAL 3) st |{p1,p6,p8}| = 0 holds
|{p1,p2,p6}| * |{p3,p6,p8}| = |{p1,p3,p6}| * |{p2,p6,p8}|

proof end;

theorem Th23: :: PASCAL:23

for p2, p4, p5, p7, p9 being Point of (TOP-REAL 3) st |{p2,p4,p9}| = 0 holds
|{p2,p4,p5}| * |{p2,p9,p7}| = - (|{p2,p4,p7}| * |{p2,p5,p9}|)

proof end;

theorem Th24: :: PASCAL:24

for p2, p4, p6, p7, p8 being Point of (TOP-REAL 3) st |{p2,p6,p7}| = 0 holds
|{p2,p4,p7}| * |{p2,p6,p8}| = - (|{p2,p4,p6}| * |{p2,p8,p7}|)

proof end;

theorem Th25: :: PASCAL:25

for p3, p4, p5, p6, p8 being Point of (TOP-REAL 3) st |{p3,p4,p8}| = 0 holds
|{p3,p4,p6}| * |{p3,p5,p8}| = |{p3,p4,p5}| * |{p3,p6,p8}|

proof end;

theorem Th26: :: PASCAL:26

for p1, p3, p5, p7, p8 being Point of (TOP-REAL 3) st |{p3,p5,p7}| = 0 holds
|{p1,p3,p5}| * |{p5,p8,p7}| = - (|{p1,p5,p7}| * |{p3,p5,p8}|)

proof end;

theorem Th27: :: PASCAL:27

for r125, r136, r246, r345, r126, r135, r245, r346, r157, r259, r597, r368, r268, r297, r247, r287, r358, r587 being non zero Real st ((r125 * r136) * r246) * r345 = ((r126 * r135) * r245) * r346 & r157 * r259 = - (r125 * r597) & r126 * r368 = r136 * r268 & r245 * r297 = - (r247 * r259) & r247 * r268 = - (r246 * r287) & r346 * r358 = r345 * r368 & r135 * r587 = - (r157 * r358) holds
r287 * r597 = r297 * r587

proof end;

theorem Th28: :: PASCAL:28

for e1, e2, e3, f1, f2, f3 being Element of F_Real
for r1, r2 being Real
for p1, p2, p3, p4, p5, p6 being Point of (TOP-REAL 3) st p1 = <*1,0,0*> & p2 = <*0,1,0*> & p3 = <*0,0,1*> & p4 = <*1,1,1*> & p5 = <*e1,e2,e3*> & p6 = <*f1,f2,f3*> & qfconic (0,0,0,r1,r2,(- (r1 + r2)),p5) = 0 & qfconic (0,0,0,r1,r2,(- (r1 + r2)),p6) = 0 holds
( qfconic (0,0,0,r1,r2,(- (r1 + r2)),p1) = 0 & qfconic (0,0,0,r1,r2,(- (r1 + r2)),p2) = 0 & qfconic (0,0,0,r1,r2,(- (r1 + r2)),p3) = 0 & qfconic (0,0,0,r1,r2,(- (r1 + r2)),p4) = 0 & ((r1 * e1) * e2) + ((r2 * e1) * e3) = ((r1 + r2) * e2) * e3 & ((r1 * f1) * f2) + ((r2 * f1) * f3) = ((r1 + r2) * f2) * f3 )

proof end;

theorem Th29: :: PASCAL:29

for e1, e2, e3, f1, f2, f3 being Element of F_Real
for r1, r2 being Real
for p1, p2, p3, p4, p5, p6, p7, p8, p9 being Point of (TOP-REAL 3) st p1 = <*1,0,0*> & p2 = <*0,1,0*> & p3 = <*0,0,1*> & p4 = <*1,1,1*> & p5 = <*e1,e2,e3*> & p6 = <*f1,f2,f3*> & |{p1,p2,p5}| <> 0 & |{p1,p3,p6}| <> 0 & |{p2,p4,p6}| <> 0 & |{p3,p4,p5}| <> 0 & |{p1,p2,p6}| <> 0 & |{p1,p3,p5}| <> 0 & |{p2,p4,p5}| <> 0 & |{p3,p4,p6}| <> 0 & |{p1,p5,p7}| <> 0 & |{p2,p5,p9}| <> 0 & |{p5,p9,p7}| <> 0 & |{p3,p6,p8}| <> 0 & |{p2,p6,p8}| <> 0 & |{p2,p9,p7}| <> 0 & |{p2,p4,p7}| <> 0 & |{p2,p8,p7}| <> 0 & |{p3,p5,p8}| <> 0 & |{p5,p8,p7}| <> 0 & ( r1 <> 0 or r2 <> 0 ) & qfconic (0,0,0,r1,r2,(- (r1 + r2)),p5) = 0 & qfconic (0,0,0,r1,r2,(- (r1 + r2)),p6) = 0 & |{p1,p5,p9}| = 0 & |{p1,p6,p8}| = 0 & |{p2,p4,p9}| = 0 & |{p2,p6,p7}| = 0 & |{p3,p4,p8}| = 0 & |{p3,p5,p7}| = 0 holds
|{p2,p8,p7}| * |{p5,p9,p7}| = |{p2,p9,p7}| * |{p5,p8,p7}|

proof end;

theorem Th30: :: PASCAL:30

for p2, p5, p7, p8, p9 being Point of (TOP-REAL 3) st |{p2,p8,p7}| * |{p5,p9,p7}| = |{p2,p9,p7}| * |{p5,p8,p7}| holds
|{p7,p2,p5}| * |{p7,p8,p9}| = 0

proof end;

::PROVER9
:: set(ignore_option_dependencies). % GUI handles dependencies
:: if(Prover9). % Options for Prover9
:: assign(max_seconds, 60).
:: end_if.
:: if(Mace4). % Options for Mace4
:: assign(max_seconds, 60).
:: end_if.
:: formulas(assumptions).
:: ((x = y) | (x = z) | (y = z)) -> f(x,y,z) #label(COLLSP2).
:: ((x != y) & f(x,y,z) & f(x,y,u) & f(x,y,v)) -> f(z,u,v) #label(COLLSP3).
:: f(x,y,x) #label(COLLSP5).
:: f(x,y,z) -> (f(y,z,x) & f(z,x,y) & f(y,x,z) & f(x,z,y) & f(z,x,y)) #label(HESSENBE1).
:: end_of_list.
:: formulas(goals).
:: -f(x1,x2,x4) & -f(x1,x2,x5) &
:: -f(x1,x6,x4) & -f(x1,x6,x5) &
:: -f(x2,x6,x4) & -f(x3,x4,x2) &
:: -f(x3,x4,x6) & -f(x3,x5,x2) &
:: -f(x3,x5,x6) & -f(x4,x5,x2) &
:: f(x1,x4,x7) & f(x1,x5,x8) &
:: f(x2,x3,x7) & f(x2,x5,x9) &
:: f(x6,x3,x8) & f(x6,x4,x9)
:: -> (-f(x9,x2,x4) & -f(x1,x4,x9) &
:: -f(x2,x3,x9) & -f(x2,x4,x7) &
:: -f(x2,x5,x8) & -f(x2,x9,x8) &
:: -f(x2,x9,x7) & -f(x6,x4,x8) &
:: -f(x6,x5,x8) & -f(x4,x9,x8) &
:: -f(x4,x9,x7)).
:: end_of_list.
:: ============================== prooftrans ============================
:: Prover9 (32) version Dec-2007, Dec 2007.
:: Process 10620 was started by RC on ,
:: Wed
:: The command was "/cygdrive/c/Program Files (x86)/Prover9-Mace4/bin-win32/prover9".
:: ============================== end of head ===========================
:: ============================== end of input ==========================
:: ============================== PROOF =================================
:: % -------- Comments from original proof --------
:: % Proof 1 at 0.36 (+ 0.09) seconds.
:: % Length of proof is 104.
:: % Level of proof is 29.
:: % Maximum clause weight is 44.
:: % Given clauses 786.
:: 1 x = y | x = z | y = z -> f(x,y,z) # label(COLLSP2) # label(non_clause). [assumption].
:: 2 x != y & f(x,y,z) & f(x,y,u) & f(x,y,w) -> f(z,u,w) # label(COLLSP3) # label(non_clause). [assumption].
:: 3 f(x,y,z) -> f(y,z,x) & f(z,x,y) & f(y,x,z) & f(x,z,y) & f(z,x,y) # label(HESSENBE1) # label(non_clause). [assumption].
:: 4 -f(x,y,z) & -f(x,y,u) & -f(x,w,z) & -f(x,w,u) & -f(y,w,z) & -f(v5,z,y) & -f(v5,z,w) & -f(v5,u,y) & -f(v5,u,w) & -f(z,u,y) & f(x,z,v6) & f(x,u,v7) & f(y,v5,v6) & f(y,u,v8) & f(w,v5,v7) & f(w,z,v8) -> -f(v8,y,z) & -f(x,z,v8) & -f(y,v5,v8) & -f(y,z,v6) & -f(y,u,v7) & -f(y,v8,v7) & -f(y,v8,v6) & -f(w,z,v7) & -f(w,u,v7) & -f(z,v8,v7) & -f(z,v8,v6) # label(non_clause) # label(goal). [goal].
:: 6 x != y | f(y,z,x) # label(COLLSP2). [clausify(1)].
:: 7 x != y | f(z,y,x) # label(COLLSP2). [clausify(1)].
:: 8 x = y | -f(y,x,z) | -f(y,x,u) | -f(y,x,w) | f(z,u,w) # label(COLLSP3). [clausify(2)].
:: 9 f(x,y,x) # label(COLLSP5). [assumption].
:: 10 -f(x,y,z) | f(y,z,x) # label(HESSENBE1). [clausify(3)].
:: 11 -f(x,y,z) | f(z,x,y) # label(HESSENBE1). [clausify(3)].
:: 12 -f(x,y,z) | f(y,x,z) # label(HESSENBE1). [clausify(3)].
:: 13 -f(x,y,z) | f(x,z,y) # label(HESSENBE1). [clausify(3)].
:: 14 -f(c1,c2,c3). [deny(4)].
:: 15 -f(c1,c2,c4). [deny(4)].
:: 16 -f(c1,c5,c3). [deny(4)].
:: 17 -f(c1,c5,c4). [deny(4)].
:: 18 -f(c2,c5,c3). [deny(4)].
:: 19 -f(c6,c3,c2). [deny(4)].
:: 20 -f(c6,c3,c5). [deny(4)].
:: 21 -f(c6,c4,c2). [deny(4)].
:: 22 -f(c6,c4,c5). [deny(4)].
:: 23 -f(c3,c4,c2). [deny(4)].
:: 24 f(c1,c3,c7). [deny(4)].
:: 25 f(c1,c4,c8). [deny(4)].
:: 26 f(c2,c6,c7). [deny(4)].
:: 27 f(c2,c4,c9). [deny(4)].
:: 28 f(c5,c6,c8). [deny(4)].
:: 29 f(c5,c3,c9). [deny(4)].
:: 30 f(c9,c2,c3) | f(c1,c3,c9) | f(c2,c6,c9) | f(c2,c3,c7) | f(c2,c4,c8) | f(c2,c9,c8) | f(c2,c9,c7) | f(c5,c3,c8) | f(c5,c4,c8) | f(c3,c9,c8) | f(c3,c9,c7). [deny(4)].
:: 34 f(x,y,y). [xx_res(7,a)].
:: 35 x = y | -f(y,x,z) | -f(y,x,u) | f(z,u,y). [resolve(9,a,8,d)].
:: 36 x = y | -f(y,x,z) | -f(y,x,u) | f(z,y,u). [resolve(9,a,8,c)].
:: 37 x = y | -f(y,x,z) | -f(y,x,u) | f(y,z,u). [resolve(9,a,8,b)].
:: 40 -f(c2,c3,c1). [ur(11,b,14,a)].
:: 42 c3 != c2. [ur(7,b,14,a)].
:: 43 c3 != c1. [ur(6,b,14,a)].
:: 49 c4 != c2. [ur(7,b,15,a)].
:: 54 -f(c3,c1,c5). [ur(10,b,16,a)].
:: 55 c5 != c3. [ur(7,b,16,a),flip(a)].
:: 57 -f(c1,c4,c5). [ur(13,b,17,a)].
:: 61 c5 != c4. [ur(7,b,17,a),flip(a)].
:: 63 -f(c5,c2,c3). [ur(12,b,18,a)].
:: 64 -f(c5,c3,c2). [ur(11,b,18,a)].
:: 70 -f(c2,c6,c3). [ur(10,b,19,a)].
:: 79 -f(c4,c6,c2). [ur(12,b,21,a)].
:: 86 -f(c5,c6,c4). [ur(10,b,22,a)].
:: 92 f(c1,c7,c3). [resolve(24,a,13,a)].
:: 99 f(c1,c8,c4). [resolve(25,a,13,a)].
:: 108 f(c7,c2,c6). [resolve(26,a,11,a)].
:: 113 f(c2,c9,c4). [resolve(27,a,13,a)].
:: 120 f(c5,c8,c6). [resolve(28,a,13,a)].
:: 127 f(c5,c9,c3). [resolve(29,a,13,a)].
:: 130 f(c3,c9,c5). [resolve(29,a,10,a)].
:: 132 -f(c5,c3,x) | -f(c5,c3,y) | f(x,c9,y). [resolve(29,a,8,c),flip(a),unit_del(a,55)].
:: 134 f(c1,c3,c9) | f(c2,c6,c9) | f(c2,c3,c7) | f(c2,c4,c8) | f(c2,c9,c8) | f(c2,c9,c7) | f(c5,c3,c8) | f(c5,c4,c8) | f(c3,c9,c8) | f(c3,c9,c7) | f(c9,c3,c2). [resolve(30,a,13,a)].
:: 142 x = y | -f(y,x,z) | -f(y,x,u) | f(z,u,x). [resolve(34,a,8,d)].
:: 144 x = y | -f(y,x,z) | -f(y,x,u) | f(x,z,u). [resolve(34,a,8,b)].
:: 145 -f(c2,c4,c3). [ur(8,a,49,a,c,34,a,d,9,a,e,23,a)].
:: 146 -f(c2,c4,c6). [ur(8,a,49,a,c,34,a,d,9,a,e,21,a)].
:: 148 -f(c4,c2,c1). [ur(8,a,49,a(flip),c,34,a,d,9,a,e,15,a)].
:: 149 -f(c3,c2,c1). [ur(8,a,42,a(flip),c,34,a,d,9,a,e,14,a)].
:: 150 f(c7,c3,c1). [resolve(92,a,10,a)].
:: 173 x = y | -f(y,x,z) | f(z,x,y). [resolve(35,c,34,a)].
:: 182 -f(c3,c5,c1). [ur(35,a,55,a,c,34,a,d,16,a)].
:: 184 -f(c4,c5,c1). [ur(35,a,61,a,c,34,a,d,17,a)].
:: 193 f(c8,c4,c1). [resolve(99,a,10,a)].
:: 310 c9 = c2 | -f(c2,c9,x) | f(c2,c4,x). [resolve(113,a,37,b)].
:: 311 c9 = c2 | -f(c2,c9,x) | f(x,c2,c4). [resolve(113,a,36,c)].
:: 314 c9 = c2 | -f(c2,c9,x) | f(c4,x,c2). [resolve(113,a,35,b)].
:: 351 c8 = c5 | -f(c5,c8,x) | f(c6,x,c5). [resolve(120,a,35,b)].
:: 389 f(c9,c3,c5). [resolve(127,a,10,a)].
:: 413 c9 = c3 | -f(c3,c9,x) | f(x,c3,c5). [resolve(130,a,36,c)].
:: 416 c9 = c3 | -f(c3,c9,x) | f(c5,x,c3). [resolve(130,a,35,b)].
:: 506 -f(c5,c3,x) | f(c3,c9,x). [resolve(132,a,34,a)].
:: 581 c9 = c3 | -f(c9,c3,x) | f(c5,x,c3). [resolve(142,b,389,a),flip(a)].
:: 751 c9 = c3 | -f(c9,c3,x) | f(c3,x,c5). [resolve(144,c,389,a),flip(a)].
:: 755 c8 = c4 | -f(c8,c4,x) | f(c4,x,c1). [resolve(144,c,193,a),flip(a)].
:: 756 c7 = c3 | -f(c7,c3,x) | f(c3,x,c1). [resolve(144,c,150,a),flip(a)].
:: 774 c7 = c2 | -f(c7,c2,x) | f(c2,x,c6). [resolve(144,c,108,a),flip(a)].
:: 797 c9 = c3 | f(c1,c3,c9) | f(c2,c6,c9) | f(c2,c3,c7) | f(c2,c4,c8) | f(c2,c9,c8) | f(c2,c9,c7) | f(c5,c3,c8) | f(c5,c4,c8) | f(c3,c9,c8) | f(c3,c9,c7). [resolve(581,b,134,k),unit_del(b,63)].
:: 799 c9 = c3 | f(c1,c3,c9) | f(c2,c6,c9) | f(c2,c3,c7) | f(c2,c4,c8) | f(c2,c9,c8) | f(c2,c9,c7) | f(c5,c3,c8) | f(c3,c9,c8) | f(c3,c9,c7) | f(c8,c4,c5). [resolve(797,i,173,b),flip(k),unit_del(k,61)].
:: 843 c9 = c3 | f(c1,c3,c9) | f(c2,c6,c9) | f(c2,c3,c7) | f(c2,c4,c8) | f(c2,c9,c8) | f(c2,c9,c7) | f(c5,c3,c8) | f(c3,c9,c8) | f(c3,c9,c7) | c8 = c4. [resolve(799,k,755,b),unit_del(l,184)].
:: 847 c9 = c3 | f(c1,c3,c9) | f(c2,c6,c9) | f(c2,c3,c7) | f(c2,c4,c8) | f(c2,c9,c8) | f(c2,c9,c7) | f(c3,c9,c8) | f(c3,c9,c7) | c8 = c4. [resolve(843,h,506,a),merge(k)].
:: 882 c9 = c3 | f(c1,c3,c9) | f(c2,c6,c9) | f(c2,c3,c7) | f(c2,c4,c8) | f(c2,c9,c8) | f(c2,c9,c7) | f(c3,c9,c7) | c8 = c4 | f(c5,c8,c3). [resolve(847,h,416,b),merge(j)].
:: 1055 c9 = c3 | f(c1,c3,c9) | f(c2,c6,c9) | f(c2,c3,c7) | f(c2,c4,c8) | f(c2,c9,c8) | f(c2,c9,c7) | f(c3,c9,c7) | c8 = c4 | c8 = c5. [resolve(882,j,351,b),unit_del(k,20)].
:: 1071 c9 = c3 | f(c1,c3,c9) | f(c2,c6,c9) | f(c2,c3,c7) | f(c2,c4,c8) | f(c2,c9,c8) | f(c2,c9,c7) | c8 = c4 | c8 = c5 | f(c7,c3,c5). [resolve(1055,h,413,b),merge(j)].
:: 1256 c9 = c3 | f(c1,c3,c9) | f(c2,c6,c9) | f(c2,c3,c7) | f(c2,c4,c8) | f(c2,c9,c8) | f(c2,c9,c7) | c8 = c4 | c8 = c5 | c7 = c3. [resolve(1071,j,756,b),unit_del(k,182)].
:: 1273 c9 = c3 | f(c1,c3,c9) | f(c2,c6,c9) | f(c2,c3,c7) | f(c2,c4,c8) | f(c2,c9,c7) | c8 = c4 | c8 = c5 | c7 = c3 | c9 = c2. [resolve(1256,f,310,b),merge(k)].
:: 1293 c9 = c3 | f(c1,c3,c9) | f(c2,c6,c9) | f(c2,c3,c7) | f(c2,c4,c8) | c8 = c4 | c8 = c5 | c7 = c3 | c9 = c2 | f(c7,c2,c4). [resolve(1273,f,311,b),merge(j)].
:: 1497 c9 = c3 | f(c1,c3,c9) | f(c2,c6,c9) | f(c2,c3,c7) | f(c2,c4,c8) | c8 = c4 | c8 = c5 | c7 = c3 | c9 = c2 | c7 = c2. [resolve(1293,j,774,b),unit_del(k,146)].
:: 1529 c9 = c3 | f(c1,c3,c9) | f(c2,c3,c7) | f(c2,c4,c8) | c8 = c4 | c8 = c5 | c7 = c3 | c9 = c2 | c7 = c2 | f(c2,c9,c6). [resolve(1497,c,13,a)].
:: 1809 c9 = c3 | f(c1,c3,c9) | f(c2,c3,c7) | f(c2,c4,c8) | c8 = c4 | c8 = c5 | c7 = c3 | c9 = c2 | c7 = c2. [resolve(1529,j,314,b),merge(j),unit_del(j,79)].
:: 1821 c9 = c3 | f(c1,c3,c9) | f(c2,c3,c7) | c8 = c4 | c8 = c5 | c7 = c3 | c9 = c2 | c7 = c2 | f(c8,c4,c2). [resolve(1809,d,173,b),unit_del(i,49)].
:: 2066 c9 = c3 | f(c1,c3,c9) | f(c2,c3,c7) | c8 = c4 | c8 = c5 | c7 = c3 | c9 = c2 | c7 = c2. [resolve(1821,i,755,b),merge(i),unit_del(i,148)].
:: 2067 c9 = c3 | f(c1,c3,c9) | c8 = c4 | c8 = c5 | c7 = c3 | c9 = c2 | c7 = c2 | f(c7,c3,c2). [resolve(2066,c,173,b),unit_del(h,42)].
:: 2087 c9 = c3 | f(c1,c3,c9) | c8 = c4 | c8 = c5 | c7 = c3 | c9 = c2 | c7 = c2. [resolve(2067,h,756,b),merge(h),unit_del(h,149)].
:: 2099 c9 = c3 | c8 = c4 | c8 = c5 | c7 = c3 | c9 = c2 | c7 = c2 | f(c9,c3,c1). [resolve(2087,b,173,b),unit_del(g,43)].
:: 2339 c9 = c3 | c8 = c4 | c8 = c5 | c7 = c3 | c9 = c2 | c7 = c2. [resolve(2099,g,751,b),merge(g),unit_del(g,54)].
:: 2346 c8 = c4 | c8 = c5 | c7 = c3 | c9 = c2 | c7 = c2. [para(2339(a,1),27(a,3)),unit_del(f,145)].
:: 2353 c8 = c4 | c8 = c5 | c7 = c3 | c7 = c2. [para(2346(d,1),29(a,3)),unit_del(e,64)].
:: 2360 c8 = c4 | c7 = c3 | c7 = c2. [para(2353(b,1),25(a,3)),unit_del(d,57)].
:: 2367 c7 = c3 | c7 = c2. [para(2360(a,1),28(a,3)),unit_del(c,86)].
:: 2374 c7 = c2. [para(2367(a,1),26(a,3)),unit_del(b,70)].
:: 2470 $F. [back_rewrite(150),rewrite([2374(1)]),unit_del(a,40)].
:: ============================== end of proof ==========================
:: OTT2MIZ (J. URBAN)

theorem Th31: :: PASCAL:31

for PCPP being CollProjectiveSpace
for c1, c2, c3, c4, c5, c6, c7, c8, c9 being Element of PCPP st not c1,c2,c4 are_collinear & not c1,c2,c5 are_collinear & not c1,c6,c4 are_collinear & not c1,c6,c5 are_collinear & not c2,c6,c4 are_collinear & not c3,c4,c2 are_collinear & not c3,c4,c6 are_collinear & not c3,c5,c2 are_collinear & not c3,c5,c6 are_collinear & not c4,c5,c2 are_collinear & c1,c4,c7 are_collinear & c1,c5,c8 are_collinear & c2,c3,c7 are_collinear & c2,c5,c9 are_collinear & c6,c3,c8 are_collinear & c6,c4,c9 are_collinear holds
( not c9,c2,c4 are_collinear & not c1,c4,c9 are_collinear & not c2,c3,c9 are_collinear & not c2,c4,c7 are_collinear & not c2,c5,c8 are_collinear & not c2,c9,c8 are_collinear & not c2,c9,c7 are_collinear & not c6,c4,c8 are_collinear & not c6,c5,c8 are_collinear & not c4,c9,c8 are_collinear & not c4,c9,c7 are_collinear )

proof end;

definition

let P1, P2, P3, P4, P5, P6, P7, P8, P9 be Point of (ProjectiveSpace (TOP-REAL 3));

pred P1,P2,P3,P4,P5,P6,P7,P8,P9 are_in_Pascal_configuration means :: PASCAL:def 4
( not P1,P2,P4 are_collinear & not P1,P3,P4 are_collinear & not P2,P3,P4 are_collinear & not P1,P2,P5 are_collinear & not P1,P2,P6 are_collinear & not P1,P3,P5 are_collinear & not P1,P3,P6 are_collinear & not P2,P4,P5 are_collinear & not P2,P4,P6 are_collinear & not P3,P4,P5 are_collinear & not P3,P4,P6 are_collinear & not P2,P3,P5 are_collinear & not P2,P3,P6 are_collinear & not P4,P5,P1 are_collinear & not P4,P6,P1 are_collinear & not P5,P6,P1 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 );

end;

:: deftheorem defines are_in_Pascal_configuration PASCAL:def 4 :
for P1, P2, P3, P4, P5, P6, P7, P8, P9 being Point of (ProjectiveSpace (TOP-REAL 3)) holds
( P1,P2,P3,P4,P5,P6,P7,P8,P9 are_in_Pascal_configuration iff ( not P1,P2,P4 are_collinear & not P1,P3,P4 are_collinear & not P2,P3,P4 are_collinear & not P1,P2,P5 are_collinear & not P1,P2,P6 are_collinear & not P1,P3,P5 are_collinear & not P1,P3,P6 are_collinear & not P2,P4,P5 are_collinear & not P2,P4,P6 are_collinear & not P3,P4,P5 are_collinear & not P3,P4,P6 are_collinear & not P2,P3,P5 are_collinear & not P2,P3,P6 are_collinear & not P4,P5,P1 are_collinear & not P4,P6,P1 are_collinear & not P5,P6,P1 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 ) );

theorem Th32: :: PASCAL:32

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 )

proof end;

theorem Th33: :: PASCAL:33

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

proof end;

theorem Th34: :: PASCAL:34

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

proof end;

registration

cluster TOP-REAL 3 -> up-3-dimensional ;

coherence
TOP-REAL 3 is up-3-dimensional

proof end;

end;

theorem Th35: :: PASCAL:35

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

proof end;

:: Pascal's theorem

theorem :: PASCAL:36

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

proof end;