let PCPP be CollProjectiveSpace; for c1, c2, c3, c4, c5, c6, c7, c8, c10 being Element of PCPP st not c2 = c1 & not c3 = c2 & not c5 = c1 & not c7 = c5 & not c7 = c6 & not c1,c4,c7 are_collinear & c1,c4,c2 are_collinear & c1,c4,c3 are_collinear & c1,c7,c5 are_collinear & c1,c7,c6 are_collinear & c4,c5,c8 are_collinear & c7,c2,c8 are_collinear & c2,c6,c10 are_collinear & c3,c5,c10 are_collinear holds
not c10,c7,c8 are_collinear
let c1, c2, c3, c4, c5, c6, c7, c8, c10 be Element of PCPP; ( not c2 = c1 & not c3 = c2 & not c5 = c1 & not c7 = c5 & not c7 = c6 & not c1,c4,c7 are_collinear & c1,c4,c2 are_collinear & c1,c4,c3 are_collinear & c1,c7,c5 are_collinear & c1,c7,c6 are_collinear & c4,c5,c8 are_collinear & c7,c2,c8 are_collinear & c2,c6,c10 are_collinear & c3,c5,c10 are_collinear implies not c10,c7,c8 are_collinear )
assume that
A1:
not c2 = c1
and
A2:
not c3 = c2
and
A3:
not c5 = c1
and
A4:
not c7 = c5
and
A5:
not c7 = c6
and
A6:
not c1,c4,c7 are_collinear
and
A7:
c1,c4,c2 are_collinear
and
A8:
c1,c4,c3 are_collinear
and
A9:
c1,c7,c5 are_collinear
and
A10:
c1,c7,c6 are_collinear
and
A11:
c4,c5,c8 are_collinear
and
A12:
c7,c2,c8 are_collinear
and
A13:
c2,c6,c10 are_collinear
and
A14:
c3,c5,c10 are_collinear
and
A15:
c10,c7,c8 are_collinear
; contradiction
A16:
not c4 = c1
by COLLSP:2, A6;
now ( not c3,c2,c5 are_collinear & ( c8 = c7 or not c7,c8,c2 are_collinear or c10,c2,c7 are_collinear ) & ( c10 = c2 or not c2,c10,c7 are_collinear or c6,c7,c2 are_collinear ) & not c7,c6,c2 are_collinear & not c7,c5,c4 are_collinear )now ( c3,c2,c4 are_collinear & ( not c1,c3,c2 are_collinear or c3,c2,c1 are_collinear ) & not c1,c5,c4 are_collinear & c1,c4,c1 are_collinear & ( for v102, v103, v100, v104 being Element of PCPP holds
( v100 = v104 or not v104,v100,v102 are_collinear or not v104,v100,v103 are_collinear or v102,v103,v104 are_collinear ) ) & c7,c8,c10 are_collinear & c2,c10,c6 are_collinear )
c1,
c4,
c4 are_collinear
by COLLSP:2;
hence
c3,
c2,
c4 are_collinear
by A8, A7, A16, COLLSP:3;
( ( not c1,c3,c2 are_collinear or c3,c2,c1 are_collinear ) & not c1,c5,c4 are_collinear & c1,c4,c1 are_collinear & ( for v102, v103, v100, v104 being Element of PCPP holds
( v100 = v104 or not v104,v100,v102 are_collinear or not v104,v100,v103 are_collinear or v102,v103,v104 are_collinear ) ) & c7,c8,c10 are_collinear & c2,c10,c6 are_collinear )thus
( not
c1,
c3,
c2 are_collinear or
c3,
c2,
c1 are_collinear )
by HESSENBE:1;
( not c1,c5,c4 are_collinear & c1,c4,c1 are_collinear & ( for v102, v103, v100, v104 being Element of PCPP holds
( v100 = v104 or not v104,v100,v102 are_collinear or not v104,v100,v103 are_collinear or v102,v103,v104 are_collinear ) ) & c7,c8,c10 are_collinear & c2,c10,c6 are_collinear )
(
c1,
c5,
c1 are_collinear &
c1,
c5,
c7 are_collinear )
by COLLSP:2, A9, HESSENBE:1;
hence
not
c1,
c5,
c4 are_collinear
by A3, COLLSP:3, A6;
( c1,c4,c1 are_collinear & ( for v102, v103, v100, v104 being Element of PCPP holds
( v100 = v104 or not v104,v100,v102 are_collinear or not v104,v100,v103 are_collinear or v102,v103,v104 are_collinear ) ) & c7,c8,c10 are_collinear & c2,c10,c6 are_collinear )thus
c1,
c4,
c1 are_collinear
by COLLSP:2;
( ( for v102, v103, v100, v104 being Element of PCPP holds
( v100 = v104 or not v104,v100,v102 are_collinear or not v104,v100,v103 are_collinear or v102,v103,v104 are_collinear ) ) & c7,c8,c10 are_collinear & c2,c10,c6 are_collinear )thus
for
v102,
v103,
v100,
v104 being
Element of
PCPP holds
(
v100 = v104 or not
v104,
v100,
v102 are_collinear or not
v104,
v100,
v103 are_collinear or
v102,
v103,
v104 are_collinear )
( c7,c8,c10 are_collinear & c2,c10,c6 are_collinear )proof
let v102,
v103,
v100,
v104 be
Element of
PCPP;
( v100 = v104 or not v104,v100,v102 are_collinear or not v104,v100,v103 are_collinear or v102,v103,v104 are_collinear )
v104,
v100,
v104 are_collinear
by COLLSP:2;
hence
(
v100 = v104 or not
v104,
v100,
v102 are_collinear or not
v104,
v100,
v103 are_collinear or
v102,
v103,
v104 are_collinear )
by COLLSP:3;
verum
end; thus
c7,
c8,
c10 are_collinear
by A15, HESSENBE:1;
c2,c10,c6 are_collinear thus
c2,
c10,
c6 are_collinear
by A13, HESSENBE:1;
verum end; hence
( not
c3,
c2,
c5 are_collinear & (
c8 = c7 or not
c7,
c8,
c2 are_collinear or
c10,
c2,
c7 are_collinear ) & (
c10 = c2 or not
c2,
c10,
c7 are_collinear or
c6,
c7,
c2 are_collinear ) )
by A7, A16, A8, A2, COLLSP:3;
( not c7,c6,c2 are_collinear & not c7,c5,c4 are_collinear )now ( c7,c6,c7 are_collinear & not c1,c2,c7 are_collinear & c7,c6,c1 are_collinear )thus
c7,
c6,
c7 are_collinear
by COLLSP:2;
( not c1,c2,c7 are_collinear & c7,c6,c1 are_collinear )
(
c1,
c2,
c1 are_collinear &
c1,
c2,
c4 are_collinear )
by COLLSP:2, A7, HESSENBE:1;
hence
not
c1,
c2,
c7 are_collinear
by A1, COLLSP:3, A6;
c7,c6,c1 are_collinear thus
c7,
c6,
c1 are_collinear
by A10, HESSENBE:1;
verum end; hence
not
c7,
c6,
c2 are_collinear
by A5, COLLSP:3;
not c7,c5,c4 are_collinear
(
c7,
c5,
c7 are_collinear &
c7,
c5,
c1 are_collinear )
by COLLSP:2, A9, HESSENBE:1;
hence
not
c7,
c5,
c4 are_collinear
by COLLSP:3, A4, A6;
verum end;
hence
contradiction
by A11, HESSENBE:1, A12, A14; verum