let PCPP be CollProjectiveSpace; for c1, c2, c3, c4, c5, c6, c7, c8, c9, c10 being Element of PCPP st c2 <> c1 & c3 <> c1 & c3 <> c2 & c4 <> c2 & c4 <> c3 & c5 <> c1 & c6 <> c1 & c6 <> c5 & c7 <> c5 & 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 & c4,c6,c9 are_collinear & c3,c7,c9 are_collinear & c2,c6,c10 are_collinear & c3,c5,c10 are_collinear holds
( not c4,c7,c2 are_collinear & not c4,c10,c3 are_collinear & not c4,c7,c3 are_collinear & not c4,c10,c2 are_collinear & not c4,c7,c5 are_collinear & not c4,c10,c8 are_collinear & not c4,c7,c8 are_collinear & not c4,c10,c5 are_collinear & not c4,c7,c9 are_collinear & not c4,c10,c6 are_collinear & not c4,c7,c6 are_collinear & not c4,c10,c9 are_collinear & not c7,c10,c5 are_collinear & not c7,c4,c6 are_collinear & not c7,c10,c9 are_collinear & not c7,c4,c3 are_collinear & not c7,c10,c3 are_collinear & not c7,c4,c9 are_collinear & not c7,c10,c2 are_collinear & not c7,c4,c8 are_collinear & not c10,c4,c2 are_collinear & not c10,c7,c6 are_collinear & not c10,c4,c6 are_collinear & not c10,c7,c2 are_collinear & not c10,c4,c5 are_collinear & not c10,c7,c3 are_collinear & not c10,c4,c3 are_collinear & not c10,c7,c5 are_collinear )
let c1, c2, c3, c4, c5, c6, c7, c8, c9, c10 be Element of PCPP; ( c2 <> c1 & c3 <> c1 & c3 <> c2 & c4 <> c2 & c4 <> c3 & c5 <> c1 & c6 <> c1 & c6 <> c5 & c7 <> c5 & 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 & c4,c6,c9 are_collinear & c3,c7,c9 are_collinear & c2,c6,c10 are_collinear & c3,c5,c10 are_collinear implies ( not c4,c7,c2 are_collinear & not c4,c10,c3 are_collinear & not c4,c7,c3 are_collinear & not c4,c10,c2 are_collinear & not c4,c7,c5 are_collinear & not c4,c10,c8 are_collinear & not c4,c7,c8 are_collinear & not c4,c10,c5 are_collinear & not c4,c7,c9 are_collinear & not c4,c10,c6 are_collinear & not c4,c7,c6 are_collinear & not c4,c10,c9 are_collinear & not c7,c10,c5 are_collinear & not c7,c4,c6 are_collinear & not c7,c10,c9 are_collinear & not c7,c4,c3 are_collinear & not c7,c10,c3 are_collinear & not c7,c4,c9 are_collinear & not c7,c10,c2 are_collinear & not c7,c4,c8 are_collinear & not c10,c4,c2 are_collinear & not c10,c7,c6 are_collinear & not c10,c4,c6 are_collinear & not c10,c7,c2 are_collinear & not c10,c4,c5 are_collinear & not c10,c7,c3 are_collinear & not c10,c4,c3 are_collinear & not c10,c7,c5 are_collinear ) )
assume that
A1:
not c2 = c1
and
A2:
not c3 = c1
and
A3:
not c3 = c2
and
A4:
not c4 = c2
and
A5:
not c4 = c3
and
A6:
not c5 = c1
and
A7:
not c6 = c1
and
A8:
not c6 = c5
and
A9:
not c7 = c5
and
A10:
not c7 = c6
and
A11:
not c1,c4,c7 are_collinear
and
A12:
c1,c4,c2 are_collinear
and
A13:
c1,c4,c3 are_collinear
and
A14:
c1,c7,c5 are_collinear
and
A15:
c1,c7,c6 are_collinear
and
A16:
c4,c5,c8 are_collinear
and
A17:
c7,c2,c8 are_collinear
and
A18:
c4,c6,c9 are_collinear
and
A19:
c3,c7,c9 are_collinear
and
A20:
c2,c6,c10 are_collinear
and
A21:
c3,c5,c10 are_collinear
and
A22:
( c4,c7,c2 are_collinear or c4,c10,c3 are_collinear or c4,c7,c3 are_collinear or c4,c10,c2 are_collinear or c4,c7,c5 are_collinear or c4,c10,c8 are_collinear or c4,c7,c8 are_collinear or c4,c10,c5 are_collinear or c4,c7,c9 are_collinear or c4,c10,c6 are_collinear or c4,c7,c6 are_collinear or c4,c10,c9 are_collinear or c7,c10,c5 are_collinear or c7,c4,c6 are_collinear or c7,c10,c9 are_collinear or c7,c4,c3 are_collinear or c7,c10,c3 are_collinear or c7,c4,c9 are_collinear or c7,c10,c2 are_collinear or c7,c4,c8 are_collinear or c10,c4,c2 are_collinear or c10,c7,c6 are_collinear or c10,c4,c6 are_collinear or c10,c7,c2 are_collinear or c10,c4,c5 are_collinear or c10,c7,c3 are_collinear or c10,c4,c3 are_collinear or c10,c7,c5 are_collinear )
; contradiction
A23:
not c7 = c1
by COLLSP:2, A11;
A24:
c4,c3,c1 are_collinear
by A13, HESSENBE:1;
A25:
c7,c5,c1 are_collinear
by A14, HESSENBE:1;
A26:
c1,c5,c7 are_collinear
by A14, HESSENBE:1;
A27:
c7,c6,c1 are_collinear
by A15, HESSENBE:1;
A28:
c1,c6,c7 are_collinear
by A15, HESSENBE:1;
A29:
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 )
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;
A30:
for v103, v104, v102, v101 being Element of PCPP holds
( v102 = v101 or not v101,v102,v103 are_collinear or not v101,v102,v104 are_collinear or v102,v103,v104 are_collinear )
proof
let v103,
v104,
v102,
v101 be
Element of
PCPP;
( v102 = v101 or not v101,v102,v103 are_collinear or not v101,v102,v104 are_collinear or v102,v103,v104 are_collinear )
v101,
v102,
v102 are_collinear
by COLLSP:2;
hence
(
v102 = v101 or not
v101,
v102,
v103 are_collinear or not
v101,
v102,
v104 are_collinear or
v102,
v103,
v104 are_collinear )
by COLLSP:3;
verum
end;
A31:
c2,c4,c1 are_collinear
by A12, HESSENBE:1;
( c4,c2,c1 are_collinear & c4,c2,c4 are_collinear )
by COLLSP:2, A12, HESSENBE:1;
then A32:
not c4,c2,c7 are_collinear
by A4, COLLSP:3, A11;
( c1,c2,c1 are_collinear & c1,c2,c4 are_collinear )
by COLLSP:2, A12, HESSENBE:1;
then A33:
not c1,c2,c7 are_collinear
by A1, COLLSP:3, A11;
c4,c3,c4 are_collinear
by COLLSP:2;
then A34:
not c4,c3,c7 are_collinear
by A24, A11, A5, COLLSP:3;
( c1,c3,c1 are_collinear & c1,c3,c4 are_collinear )
by COLLSP:2, A13, HESSENBE:1;
then A35:
not c1,c3,c7 are_collinear
by A2, COLLSP:3, A11;
c7,c5,c7 are_collinear
by COLLSP:2;
then A36:
not c7,c5,c4 are_collinear
by A25, A9, COLLSP:3, A11;
c7,c5,c7 are_collinear
by COLLSP:2;
then A37:
not c7,c5,c2 are_collinear
by A9, A25, COLLSP:3, A33;
A38:
c1,c5,c1 are_collinear
by COLLSP:2;
c7,c6,c7 are_collinear
by COLLSP:2;
then A39:
not c7,c6,c4 are_collinear
by A10, COLLSP:3, A27, A11;
c7,c6,c7 are_collinear
by COLLSP:2;
then A40:
not c7,c6,c2 are_collinear
by A27, A10, COLLSP:3, A33;
A41:
c8,c4,c5 are_collinear
by A16, HESSENBE:1;
A42:
c9,c4,c6 are_collinear
by A18, HESSENBE:1;
A43:
c10,c2,c6 are_collinear
by A20, HESSENBE:1;
A44:
c10,c3,c5 are_collinear
by A21, HESSENBE:1;
A45:
c10,c5,c3 are_collinear
by A21, HESSENBE:1;
( c3,c4,c4 are_collinear & c3,c4,c1 are_collinear )
by COLLSP:2, A13, HESSENBE:1;
then A46:
( not c3,c4,c5 are_collinear or c1,c5,c4 are_collinear )
by A5, COLLSP:3;
( c5,c7,c7 are_collinear & c5,c7,c1 are_collinear )
by COLLSP:2, A14, HESSENBE:1;
then A47:
not c5,c7,c3 are_collinear
by A35, A9, COLLSP:3;
now ( c2,c4,c4 are_collinear & not c1,c6,c4 are_collinear )thus
c2,
c4,
c4 are_collinear
by COLLSP:2;
not c1,c6,c4 are_collinear
c1,
c6,
c1 are_collinear
by COLLSP:2;
hence
not
c1,
c6,
c4 are_collinear
by A7, COLLSP:3, A28, A11;
verum end;
then A48:
not c2,c4,c6 are_collinear
by A4, COLLSP:3, A31;
A49:
for v2, v101, v100 being Element of PCPP holds
( v101 = v100 or not v100,v101,v2 are_collinear or v2,v100,v101 are_collinear )
proof
let v2,
v101,
v100 be
Element of
PCPP;
( v101 = v100 or not v100,v101,v2 are_collinear or v2,v100,v101 are_collinear )
for
v102,
v104,
v100,
v103 being
Element of
PCPP holds
(
v100 = v103 or not
v103,
v100,
v102 are_collinear or not
v103,
v100,
v104 are_collinear or
v102,
v103,
v104 are_collinear )
proof
let v102,
v104,
v100,
v103 be
Element of
PCPP;
( v100 = v103 or not v103,v100,v102 are_collinear or not v103,v100,v104 are_collinear or v102,v103,v104 are_collinear )
v103,
v100,
v103 are_collinear
by COLLSP:2;
hence
(
v100 = v103 or not
v103,
v100,
v102 are_collinear or not
v103,
v100,
v104 are_collinear or
v102,
v103,
v104 are_collinear )
by COLLSP:3;
verum
end;
then
(
v101 = v100 or not
v100,
v101,
v2 are_collinear or not
v100,
v101,
v101 are_collinear or
v2,
v100,
v101 are_collinear )
;
hence
(
v101 = v100 or not
v100,
v101,
v2 are_collinear or
v2,
v100,
v101 are_collinear )
by COLLSP:2;
verum
end;
A50:
( not c7,c6,c5 are_collinear or c6,c5,c7 are_collinear )
by HESSENBE:1;
now ( ( c4,c7,c8 are_collinear or c9 = c7 or c10 = c5 or c10 = c3 or c10 = c2 or c1,c10,c5 are_collinear or c9 = c4 or c8 = c4 or c10 = c6 or c9,c4,c7 are_collinear ) & ( c7 = c4 or not c4,c7,c8 are_collinear or c8,c4,c7 are_collinear ) & ( not c1,c10,c5 are_collinear or c10,c5,c1 are_collinear ) & not c2,c6,c5 are_collinear & ( ( not c3,c2,c6 are_collinear & not c3,c2,c5 are_collinear ) or c1,c5,c3 are_collinear ) & ( for v102, v103, v104, v101 being Element of PCPP holds
( v104 = v101 or not v101,v104,v102 are_collinear or not v101,v104,v103 are_collinear or v102,v103,v104 are_collinear ) ) & not c5,c1,c3 are_collinear & c8,c2,c7 are_collinear & not c3,c7,c4 are_collinear )now ( ( c4,c10,c3 are_collinear or c4,c10,c2 are_collinear or c4,c10,c8 are_collinear or c4,c7,c8 are_collinear or c4,c10,c5 are_collinear or c4,c7,c9 are_collinear or c4,c10,c6 are_collinear or c4,c10,c9 are_collinear or c7,c10,c3 are_collinear or c7,c4,c9 are_collinear or c7,c10,c2 are_collinear or c7,c4,c8 are_collinear or c7,c6,c10 are_collinear or c9 = c7 or c10,c5,c7 are_collinear ) & ( not c10,c8,c4 are_collinear or c8,c4,c10 are_collinear ) & ( not c4,c10,c6 are_collinear or c10,c6,c4 are_collinear ) & ( not c4,c10,c5 are_collinear or c10,c5,c4 are_collinear ) & ( not c7,c10,c3 are_collinear or c10,c3,c7 are_collinear ) & ( not c7,c10,c2 are_collinear or c10,c2,c7 are_collinear ) & ( not c10,c9,c4 are_collinear or c9,c4,c10 are_collinear ) & not c6,c4,c2 are_collinear & c7,c6,c5 are_collinear & not c5,c4,c3 are_collinear & not c3,c7,c5 are_collinear & not c2,c7,c6 are_collinear & c10,c6,c2 are_collinear )
(
c9,
c7,
c3 are_collinear & ( not
c10,
c9,
c7 are_collinear or
c9,
c7,
c10 are_collinear ) )
by A19, HESSENBE:1;
hence
(
c4,
c10,
c3 are_collinear or
c4,
c10,
c2 are_collinear or
c4,
c10,
c8 are_collinear or
c4,
c7,
c8 are_collinear or
c4,
c10,
c5 are_collinear or
c4,
c7,
c9 are_collinear or
c4,
c10,
c6 are_collinear or
c4,
c10,
c9 are_collinear or
c7,
c10,
c3 are_collinear or
c7,
c4,
c9 are_collinear or
c7,
c10,
c2 are_collinear or
c7,
c4,
c8 are_collinear or
c7,
c6,
c10 are_collinear or
c9 = c7 or
c10,
c5,
c7 are_collinear )
by A30, A39, A36, A34, A32, A22, HESSENBE:1;
( ( not c10,c8,c4 are_collinear or c8,c4,c10 are_collinear ) & ( not c4,c10,c6 are_collinear or c10,c6,c4 are_collinear ) & ( not c4,c10,c5 are_collinear or c10,c5,c4 are_collinear ) & ( not c7,c10,c3 are_collinear or c10,c3,c7 are_collinear ) & ( not c7,c10,c2 are_collinear or c10,c2,c7 are_collinear ) & ( not c10,c9,c4 are_collinear or c9,c4,c10 are_collinear ) & not c6,c4,c2 are_collinear & c7,c6,c5 are_collinear & not c5,c4,c3 are_collinear & not c3,c7,c5 are_collinear & not c2,c7,c6 are_collinear & c10,c6,c2 are_collinear )thus
( not
c10,
c8,
c4 are_collinear or
c8,
c4,
c10 are_collinear )
by HESSENBE:1;
( ( not c4,c10,c6 are_collinear or c10,c6,c4 are_collinear ) & ( not c4,c10,c5 are_collinear or c10,c5,c4 are_collinear ) & ( not c7,c10,c3 are_collinear or c10,c3,c7 are_collinear ) & ( not c7,c10,c2 are_collinear or c10,c2,c7 are_collinear ) & ( not c10,c9,c4 are_collinear or c9,c4,c10 are_collinear ) & not c6,c4,c2 are_collinear & c7,c6,c5 are_collinear & not c5,c4,c3 are_collinear & not c3,c7,c5 are_collinear & not c2,c7,c6 are_collinear & c10,c6,c2 are_collinear )thus
( not
c4,
c10,
c6 are_collinear or
c10,
c6,
c4 are_collinear )
by HESSENBE:1;
( ( not c4,c10,c5 are_collinear or c10,c5,c4 are_collinear ) & ( not c7,c10,c3 are_collinear or c10,c3,c7 are_collinear ) & ( not c7,c10,c2 are_collinear or c10,c2,c7 are_collinear ) & ( not c10,c9,c4 are_collinear or c9,c4,c10 are_collinear ) & not c6,c4,c2 are_collinear & c7,c6,c5 are_collinear & not c5,c4,c3 are_collinear & not c3,c7,c5 are_collinear & not c2,c7,c6 are_collinear & c10,c6,c2 are_collinear )thus
( not
c4,
c10,
c5 are_collinear or
c10,
c5,
c4 are_collinear )
by HESSENBE:1;
( ( not c7,c10,c3 are_collinear or c10,c3,c7 are_collinear ) & ( not c7,c10,c2 are_collinear or c10,c2,c7 are_collinear ) & ( not c10,c9,c4 are_collinear or c9,c4,c10 are_collinear ) & not c6,c4,c2 are_collinear & c7,c6,c5 are_collinear & not c5,c4,c3 are_collinear & not c3,c7,c5 are_collinear & not c2,c7,c6 are_collinear & c10,c6,c2 are_collinear )thus
( not
c7,
c10,
c3 are_collinear or
c10,
c3,
c7 are_collinear )
by HESSENBE:1;
( ( not c7,c10,c2 are_collinear or c10,c2,c7 are_collinear ) & ( not c10,c9,c4 are_collinear or c9,c4,c10 are_collinear ) & not c6,c4,c2 are_collinear & c7,c6,c5 are_collinear & not c5,c4,c3 are_collinear & not c3,c7,c5 are_collinear & not c2,c7,c6 are_collinear & c10,c6,c2 are_collinear )thus
( not
c7,
c10,
c2 are_collinear or
c10,
c2,
c7 are_collinear )
by HESSENBE:1;
( ( not c10,c9,c4 are_collinear or c9,c4,c10 are_collinear ) & not c6,c4,c2 are_collinear & c7,c6,c5 are_collinear & not c5,c4,c3 are_collinear & not c3,c7,c5 are_collinear & not c2,c7,c6 are_collinear & c10,c6,c2 are_collinear )thus
( not
c10,
c9,
c4 are_collinear or
c9,
c4,
c10 are_collinear )
by HESSENBE:1;
( not c6,c4,c2 are_collinear & c7,c6,c5 are_collinear & not c5,c4,c3 are_collinear & not c3,c7,c5 are_collinear & not c2,c7,c6 are_collinear & c10,c6,c2 are_collinear )now ( c6,c4,c6 are_collinear & not c4 = c6 & ( for v102, v104, v103, v101 being Element of PCPP holds
( v103 = v101 or not v101,v103,v102 are_collinear or not v101,v103,v104 are_collinear or v102,v103,v104 are_collinear ) ) )thus
c6,
c4,
c6 are_collinear
by COLLSP:2;
( not c4 = c6 & ( for v102, v104, v103, v101 being Element of PCPP holds
( v103 = v101 or not v101,v103,v102 are_collinear or not v101,v103,v104 are_collinear or v102,v103,v104 are_collinear ) ) )thus
not
c4 = c6
by COLLSP:2, A39;
for v102, v104, v103, v101 being Element of PCPP holds
( v103 = v101 or not v101,v103,v102 are_collinear or not v101,v103,v104 are_collinear or v102,v103,v104 are_collinear )thus
for
v102,
v104,
v103,
v101 being
Element of
PCPP holds
(
v103 = v101 or not
v101,
v103,
v102 are_collinear or not
v101,
v103,
v104 are_collinear or
v102,
v103,
v104 are_collinear )
verumproof
let v102,
v104,
v103,
v101 be
Element of
PCPP;
( v103 = v101 or not v101,v103,v102 are_collinear or not v101,v103,v104 are_collinear or v102,v103,v104 are_collinear )
v101,
v103,
v103 are_collinear
by COLLSP:2;
hence
(
v103 = v101 or not
v101,
v103,
v102 are_collinear or not
v101,
v103,
v104 are_collinear or
v102,
v103,
v104 are_collinear )
by COLLSP:3;
verum
end; end; hence
not
c6,
c4,
c2 are_collinear
by A48;
( c7,c6,c5 are_collinear & not c5,c4,c3 are_collinear & not c3,c7,c5 are_collinear & not c2,c7,c6 are_collinear & c10,c6,c2 are_collinear )
c1,
c7,
c7 are_collinear
by COLLSP:2;
hence
c7,
c6,
c5 are_collinear
by A23, A14, COLLSP:3, A15;
( not c5,c4,c3 are_collinear & not c3,c7,c5 are_collinear & not c2,c7,c6 are_collinear & c10,c6,c2 are_collinear )now ( c5,c4,c4 are_collinear & ( not c4,c3,c5 are_collinear or c1,c5,c4 are_collinear ) )thus
c5,
c4,
c4 are_collinear
by COLLSP:2;
( not c4,c3,c5 are_collinear or c1,c5,c4 are_collinear )
c4,
c3,
c4 are_collinear
by COLLSP:2;
hence
( not
c4,
c3,
c5 are_collinear or
c1,
c5,
c4 are_collinear )
by A24, A5, COLLSP:3;
verum end; hence
not
c5,
c4,
c3 are_collinear
by A29, A38, COLLSP:3, A6, A26, A11;
( not c3,c7,c5 are_collinear & not c2,c7,c6 are_collinear & c10,c6,c2 are_collinear )
c7,
c5,
c7 are_collinear
by COLLSP:2;
then
not
c7,
c5,
c3 are_collinear
by A35, A9, A25, COLLSP:3;
hence
not
c3,
c7,
c5 are_collinear
by HESSENBE:1;
( not c2,c7,c6 are_collinear & c10,c6,c2 are_collinear )thus
not
c2,
c7,
c6 are_collinear
by HESSENBE:1, A40;
c10,c6,c2 are_collinear thus
c10,
c6,
c2 are_collinear
by A20, HESSENBE:1;
verum then
(
c4,
c10,
c2 are_collinear or
c4,
c7,
c8 are_collinear or
c4,
c7,
c9 are_collinear or
c9 = c7 or
c10 = c5 or
c10 = c3 or
c10 = c2 or
c1,
c10,
c5 are_collinear or
c9 = c4 or
c8 = c4 or
c10 = c6 or
c10,
c3,
c4 are_collinear )
by A30, A45, A41, A43, A44, A47, A10, A27, COLLSP:3, A42, HESSENBE:1;
then A51:
(
c4,
c7,
c8 are_collinear or
c4,
c7,
c9 are_collinear or
c9 = c7 or
c10 = c5 or
c10 = c3 or
c10 = c2 or
c1,
c10,
c5 are_collinear or
c9 = c4 or
c8 = c4 or
c10 = c6 or
c10,
c2,
c4 are_collinear )
by A46, A38, COLLSP:3, A6, A26, A11, A30, A44, HESSENBE:1;
not
c7 = c4
by COLLSP:2, A11;
hence
(
c4,
c7,
c8 are_collinear or
c9 = c7 or
c10 = c5 or
c10 = c3 or
c10 = c2 or
c1,
c10,
c5 are_collinear or
c9 = c4 or
c8 = c4 or
c10 = c6 or
c9,
c4,
c7 are_collinear )
by A51, A49, A48, A43, A30;
( ( c7 = c4 or not c4,c7,c8 are_collinear or c8,c4,c7 are_collinear ) & ( not c1,c10,c5 are_collinear or c10,c5,c1 are_collinear ) & not c2,c6,c5 are_collinear & ( ( not c3,c2,c6 are_collinear & not c3,c2,c5 are_collinear ) or c1,c5,c3 are_collinear ) & ( for v102, v103, v104, v101 being Element of PCPP holds
( v104 = v101 or not v101,v104,v102 are_collinear or not v101,v104,v103 are_collinear or v102,v103,v104 are_collinear ) ) & not c5,c1,c3 are_collinear & c8,c2,c7 are_collinear & not c3,c7,c4 are_collinear )thus
(
c7 = c4 or not
c4,
c7,
c8 are_collinear or
c8,
c4,
c7 are_collinear )
by A49;
( ( not c1,c10,c5 are_collinear or c10,c5,c1 are_collinear ) & not c2,c6,c5 are_collinear & ( ( not c3,c2,c6 are_collinear & not c3,c2,c5 are_collinear ) or c1,c5,c3 are_collinear ) & ( for v102, v103, v104, v101 being Element of PCPP holds
( v104 = v101 or not v101,v104,v102 are_collinear or not v101,v104,v103 are_collinear or v102,v103,v104 are_collinear ) ) & not c5,c1,c3 are_collinear & c8,c2,c7 are_collinear & not c3,c7,c4 are_collinear )thus
( not
c1,
c10,
c5 are_collinear or
c10,
c5,
c1 are_collinear )
by HESSENBE:1;
( not c2,c6,c5 are_collinear & ( ( not c3,c2,c6 are_collinear & not c3,c2,c5 are_collinear ) or c1,c5,c3 are_collinear ) & ( for v102, v103, v104, v101 being Element of PCPP holds
( v104 = v101 or not v101,v104,v102 are_collinear or not v101,v104,v103 are_collinear or v102,v103,v104 are_collinear ) ) & not c5,c1,c3 are_collinear & c8,c2,c7 are_collinear & not c3,c7,c4 are_collinear )A52:
not
c4 = c1
by COLLSP:2, A11;
( ( not
c6,
c5,
c2 are_collinear or
c5,
c2,
c7 are_collinear ) &
c2,
c6,
c2 are_collinear & not
c4 = c1 & not
c6 = c2 &
c5,
c2,
c2 are_collinear &
c5,
c2,
c5 are_collinear & not
c2 = c5 )
by A40, A11, A50, A30, A8, A23, A14, A15, COLLSP:2;
hence
not
c2,
c6,
c5 are_collinear
by A30, COLLSP:3, A37;
( ( ( not c3,c2,c6 are_collinear & not c3,c2,c5 are_collinear ) or c1,c5,c3 are_collinear ) & ( for v102, v103, v104, v101 being Element of PCPP holds
( v104 = v101 or not v101,v104,v102 are_collinear or not v101,v104,v103 are_collinear or v102,v103,v104 are_collinear ) ) & not c5,c1,c3 are_collinear & c8,c2,c7 are_collinear & not c3,c7,c4 are_collinear )now ( c3,c2,c1 are_collinear & not c1,c6,c3 are_collinear )
c1,
c4,
c1 are_collinear
by COLLSP:2;
hence
c3,
c2,
c1 are_collinear
by A52, A12, COLLSP:3, A13;
not c1,c6,c3 are_collinear
c1,
c6,
c1 are_collinear
by COLLSP:2;
hence
not
c1,
c6,
c3 are_collinear
by A35, A7, A28, COLLSP:3;
verum end; hence
( ( not
c3,
c2,
c6 are_collinear & not
c3,
c2,
c5 are_collinear ) or
c1,
c5,
c3 are_collinear )
by A29, A3;
( ( for v102, v103, v104, v101 being Element of PCPP holds
( v104 = v101 or not v101,v104,v102 are_collinear or not v101,v104,v103 are_collinear or v102,v103,v104 are_collinear ) ) & not c5,c1,c3 are_collinear & c8,c2,c7 are_collinear & not c3,c7,c4 are_collinear )thus
for
v102,
v103,
v104,
v101 being
Element of
PCPP holds
(
v104 = v101 or not
v101,
v104,
v102 are_collinear or not
v101,
v104,
v103 are_collinear or
v102,
v103,
v104 are_collinear )
( not c5,c1,c3 are_collinear & c8,c2,c7 are_collinear & not c3,c7,c4 are_collinear )proof
let v102,
v103,
v104,
v101 be
Element of
PCPP;
( v104 = v101 or not v101,v104,v102 are_collinear or not v101,v104,v103 are_collinear or v102,v103,v104 are_collinear )
v101,
v104,
v104 are_collinear
by COLLSP:2;
hence
(
v104 = v101 or not
v101,
v104,
v102 are_collinear or not
v101,
v104,
v103 are_collinear or
v102,
v103,
v104 are_collinear )
by COLLSP:3;
verum
end;
(
c5,
c1,
c1 are_collinear &
c5,
c1,
c7 are_collinear )
by COLLSP:2, A14, HESSENBE:1;
hence
not
c5,
c1,
c3 are_collinear
by A35, A6, COLLSP:3;
( c8,c2,c7 are_collinear & not c3,c7,c4 are_collinear )thus
c8,
c2,
c7 are_collinear
by A17, HESSENBE:1;
not c3,c7,c4 are_collinear
(
c3,
c7,
c7 are_collinear &
c3,
c7,
c3 are_collinear & not
c7 = c3 )
by COLLSP:2, A34;
hence
not
c3,
c7,
c4 are_collinear
by COLLSP:3, A34;
verum
hence
contradiction
by A30, A45, HESSENBE:1, A36, A42, COLLSP:2, A41, A23, A14, A15, A50, A47, A32, A39, A19, A20; verum