let P1, P2, P3, P4, P5, P6, P7, P8, P9 be 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
let a, b, c, d, e, f be Real; ( ( 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 implies P7,P8,P9 are_collinear )
per cases
( P1,P2,P3 are_collinear or not P1,P2,P3 are_collinear )
;
suppose
P1,
P2,
P3 are_collinear
;
( ( 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 implies P7,P8,P9 are_collinear )hence
( ( 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 implies
P7,
P8,
P9 are_collinear )
by Th35;
verum end; suppose
not
P1,
P2,
P3 are_collinear
;
( ( 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 implies P7,P8,P9 are_collinear )hence
( ( 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 implies
P7,
P8,
P9 are_collinear )
by Th34;
verum end; end;