let PCPP be 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 )
let c1, c2, c3, c4, c5, c6, c7, c8, c9 be Element of PCPP; ( 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 implies ( 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 ) )
assume that
A11:
not c1,c2,c4 are_collinear
and
A12:
not c1,c2,c5 are_collinear
and
A13:
not c1,c6,c4 are_collinear
and
A14:
not c1,c6,c5 are_collinear
and
A15:
not c2,c6,c4 are_collinear
and
A16:
not c3,c4,c2 are_collinear
and
A17:
not c3,c4,c6 are_collinear
and
A18:
not c3,c5,c2 are_collinear
and
A19:
not c3,c5,c6 are_collinear
and
A20:
not c4,c5,c2 are_collinear
and
A21:
c1,c4,c7 are_collinear
and
A22:
c1,c5,c8 are_collinear
and
A23:
c2,c3,c7 are_collinear
and
A24:
c2,c5,c9 are_collinear
and
A25:
c6,c3,c8 are_collinear
and
A26:
c6,c4,c9 are_collinear
and
A27:
( c9,c2,c4 are_collinear or c1,c4,c9 are_collinear or c2,c3,c9 are_collinear or c2,c4,c7 are_collinear or c2,c5,c8 are_collinear or c2,c9,c8 are_collinear or c2,c9,c7 are_collinear or c6,c4,c8 are_collinear or c6,c5,c8 are_collinear or c4,c9,c8 are_collinear or c4,c9,c7 are_collinear )
; contradiction
A34:
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:5;
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;
A38:
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:5;
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;
A47:
not c5 = c2
by COLLSP:2, A12;
A49:
not c6,c4,c1 are_collinear
by HESSENBE:1, A13;
A51:
not c4,c1,c6 are_collinear
by HESSENBE:1, A13;
A54:
not c6 = c4
by A13, COLLSP:2;
A61:
not c6,c4,c2 are_collinear
by HESSENBE:1, A15;
A67:
not c6,c3,c4 are_collinear
by HESSENBE:1, A17;
A69:
not c2,c3,c5 are_collinear
by HESSENBE:1, A18;
A75:
c4,c7,c1 are_collinear
by A21, HESSENBE:1;
A79:
c2,c7,c3 are_collinear
by A23, COLLSP:4;
A81:
c9,c2,c5 are_collinear
by A24, HESSENBE:1;
A83:
c2,c9,c5 are_collinear
by A24, COLLSP:4;
A85:
c6,c8,c3 are_collinear
by A25, COLLSP:4;
A89:
c4,c9,c6 are_collinear
by A26, HESSENBE:1;
A98:
( c1,c4,c9 are_collinear or c2,c3,c9 are_collinear or c2,c4,c7 are_collinear or c2,c5,c8 are_collinear or c2,c9,c8 are_collinear or c2,c9,c7 are_collinear or c6,c4,c8 are_collinear or c6,c5,c8 are_collinear or c4,c9,c8 are_collinear or c4,c9,c7 are_collinear or c9,c4,c2 are_collinear )
by A27, COLLSP:4;
A101:
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 )
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;
A105:
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;
A121:
c7,c4,c1 are_collinear
by A21, HESSENBE:1;
A124:
for v2, v101, v100 being Element of PCPP holds
( v101 = v100 or not v100,v101,v2 are_collinear or v2,v101,v100 are_collinear )
proof
let v2,
v101,
v100 be
Element of
PCPP;
( v101 = v100 or not v100,v101,v2 are_collinear or v2,v101,v100 are_collinear )
(
v101 = v100 or not
v100,
v101,
v2 are_collinear or not
v100,
v101,
v101 are_collinear or
v2,
v101,
v100 are_collinear )
by A34;
hence
(
v101 = v100 or not
v100,
v101,
v2 are_collinear or
v2,
v101,
v100 are_collinear )
by COLLSP:2;
verum
end;
A130:
c2,c5,c5 are_collinear
by COLLSP:2;
A133:
not c2,c5,c4 are_collinear
by A130, A47, A34, A20;
A144:
c8,c5,c1 are_collinear
by A22, HESSENBE:1;
A147:
for v0 being Element of PCPP holds
( c7 = c4 or not c4,c7,v0 are_collinear or v0,c4,c1 are_collinear )
by A75, A38;
A158:
for v0 being Element of PCPP holds
( c7 = c2 or not c2,c7,v0 are_collinear or c2,c3,v0 are_collinear )
by A79, HESSENBE:2;
A161:
for v0 being Element of PCPP holds
( c9 = c2 or not c2,c9,v0 are_collinear or c2,v0,c5 are_collinear )
by A83, HESSENBE:2;
A169:
c9,c4,c6 are_collinear
by A26, HESSENBE:1;
A175:
for v0 being Element of PCPP holds
( c9 = c4 or not c4,c9,v0 are_collinear or c4,v0,c6 are_collinear )
by A89, HESSENBE:2;
A203:
( c5 = c6 or not c6,c5,c8 are_collinear or c8,c5,c6 are_collinear )
by A124;
A213:
( c9 = c4 or not c4,c9,c8 are_collinear or c6,c8,c4 are_collinear )
by A89, A34;
A234:
( c5 = c2 or not c2,c5,c8 are_collinear or c8,c5,c2 are_collinear )
by A124;
A241:
( c4 = c2 or not c2,c4,c7 are_collinear or c7,c4,c2 are_collinear )
by A124;
A247:
( c9 = c4 or c1,c4,c9 are_collinear or c2,c3,c9 are_collinear or c8 = c5 or c8 = c6 or c7 = c4 or c9 = c2 or c7 = c2 )
by A11, A121, A105, COLLSP:2, A12, A69, A158, A49, A175, A67, A54, A26, A14, A144, A15, A98, A169, A101, A203, A213, A85, A147, A83, HESSENBE:2, A161, A241, A234;
A248:
( not c2,c3,c9 are_collinear or c9,c2,c3 are_collinear )
by HESSENBE:1;
( c4 = c1 or not c1,c4,c9 are_collinear or c9,c4,c1 are_collinear )
by A124;
hence
contradiction
by A11, A21, A16, HESSENBE:1, A23, A19, A25, A14, A22, A61, A26, A133, A24, A51, A169, COLLSP:2, A69, A247, A248, A81, A105; verum