let PCPP be CollProjectiveSpace; for c1, c2, c3, c4, c5, c6, c7 being Element of PCPP st c3 <> c1 & c4 <> c1 & c4 <> c3 & c3 <> c2 & c4 <> c2 & c6 <> c1 & c7 <> c1 & c7 <> c6 & c6 <> c5 & c7 <> c5 & not c1,c2,c5 are_collinear & c1,c2,c3 are_collinear & c1,c2,c4 are_collinear & c1,c5,c6 are_collinear & c1,c5,c7 are_collinear holds
( not c1,c3,c6 are_collinear & c1,c3,c4 are_collinear & c1,c6,c7 are_collinear & c3 <> c1 & c2 <> c1 & c3 <> c2 & c4 <> c3 & c4 <> c2 & c6 <> c1 & c5 <> c1 & c6 <> c5 & c7 <> c6 & c7 <> c5 & not c1,c4,c7 are_collinear & c1,c4,c3 are_collinear & c1,c4,c2 are_collinear & c1,c7,c6 are_collinear & c1,c7,c5 are_collinear )
let c1, c2, c3, c4, c5, c6, c7 be Element of PCPP; ( c3 <> c1 & c4 <> c1 & c4 <> c3 & c3 <> c2 & c4 <> c2 & c6 <> c1 & c7 <> c1 & c7 <> c6 & c6 <> c5 & c7 <> c5 & not c1,c2,c5 are_collinear & c1,c2,c3 are_collinear & c1,c2,c4 are_collinear & c1,c5,c6 are_collinear & c1,c5,c7 are_collinear implies ( not c1,c3,c6 are_collinear & c1,c3,c4 are_collinear & c1,c6,c7 are_collinear & c3 <> c1 & c2 <> c1 & c3 <> c2 & c4 <> c3 & c4 <> c2 & c6 <> c1 & c5 <> c1 & c6 <> c5 & c7 <> c6 & c7 <> c5 & not c1,c4,c7 are_collinear & c1,c4,c3 are_collinear & c1,c4,c2 are_collinear & c1,c7,c6 are_collinear & c1,c7,c5 are_collinear ) )
assume that
A1:
not c3 = c1
and
A2:
not c4 = c1
and
A3:
not c4 = c3
and
A4:
not c3 = c2
and
A5:
not c4 = c2
and
A6:
not c6 = c1
and
A7:
not c7 = c1
and
A8:
not c7 = c6
and
A9:
not c6 = c5
and
A10:
not c7 = c5
and
A11:
not c1,c2,c5 are_collinear
and
A12:
c1,c2,c3 are_collinear
and
A13:
c1,c2,c4 are_collinear
and
A14:
c1,c5,c6 are_collinear
and
A15:
c1,c5,c7 are_collinear
and
A16:
( c1,c3,c6 are_collinear or not c1,c3,c4 are_collinear or not c1,c6,c7 are_collinear or c3 = c1 or c2 = c1 or c3 = c2 or c4 = c3 or c4 = c2 or c6 = c1 or c5 = c1 or c6 = c5 or c7 = c6 or c7 = c5 or c1,c4,c7 are_collinear or not c1,c4,c3 are_collinear or not c1,c4,c2 are_collinear or not c1,c7,c6 are_collinear or not c1,c7,c5 are_collinear )
; contradiction
A17:
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;
A18:
not c5 = c1
by COLLSP:2, A11;
A19:
not c2 = c1
by COLLSP:2, A11;
A20:
c3,c1,c2 are_collinear
by A12, HESSENBE:1;
A21:
c4,c1,c2 are_collinear
by A13, HESSENBE:1;
A22:
c6,c1,c5 are_collinear
by A14, HESSENBE:1;
A23:
c7,c1,c5 are_collinear
by A15, HESSENBE:1;
A24:
c3,c1,c1 are_collinear
by COLLSP:2;
A25:
not c3,c1,c5 are_collinear
by A24, A20, COLLSP:3, A11, A1;
now ( c4,c1,c1 are_collinear & not c6,c1,c3 are_collinear & ( not c7,c1,c4 are_collinear or c4,c1,c5 are_collinear ) & c1,c3,c3 are_collinear & c1,c4,c4 are_collinear )thus
c4,
c1,
c1 are_collinear
by COLLSP:2;
( not c6,c1,c3 are_collinear & ( not c7,c1,c4 are_collinear or c4,c1,c5 are_collinear ) & c1,c3,c3 are_collinear & c1,c4,c4 are_collinear )
c6,
c1,
c1 are_collinear
by COLLSP:2;
hence
not
c6,
c1,
c3 are_collinear
by A22, A6, COLLSP:3, A25;
( ( not c7,c1,c4 are_collinear or c4,c1,c5 are_collinear ) & c1,c3,c3 are_collinear & c1,c4,c4 are_collinear )
c7,
c1,
c1 are_collinear
by COLLSP:2;
hence
( not
c7,
c1,
c4 are_collinear or
c4,
c1,
c5 are_collinear )
by A23, COLLSP:3, A7;
( c1,c3,c3 are_collinear & c1,c4,c4 are_collinear )thus
c1,
c3,
c3 are_collinear
by COLLSP:2;
c1,c4,c4 are_collinear thus
c1,
c4,
c4 are_collinear
by COLLSP:2;
verum end;
hence
contradiction
by A13, COLLSP:4, COLLSP:2, A10, A8, A9, A5, A3, A4, A16, A15, A17, A1, A19, A12, A18, A14, HESSENBE:2, A21, A2, COLLSP:3, A11; verum