let PCPP be CollProjectiveSpace; for c1, c2, c4, c5, c6, c8 being Element of PCPP st c4 <> c2 & c6 <> c1 & not c1,c2,c5 are_collinear & c1,c2,c4 are_collinear & c1,c5,c6 are_collinear & c4,c6,c8 are_collinear holds
c8 <> c2
let c1, c2, c4, c5, c6, c8 be Element of PCPP; ( c4 <> c2 & c6 <> c1 & not c1,c2,c5 are_collinear & c1,c2,c4 are_collinear & c1,c5,c6 are_collinear & c4,c6,c8 are_collinear implies c8 <> c2 )
assume that
A1:
not c4 = c2
and
A2:
not c6 = c1
and
A3:
not c1,c2,c5 are_collinear
and
A4:
c1,c2,c4 are_collinear
and
A5:
c1,c5,c6 are_collinear
and
A6:
c4,c6,c8 are_collinear
and
A7:
c8 = c2
; contradiction
now ( not c6,c1,c2 are_collinear & ( for v3, v2 being Element of PCPP holds
( c4 = c2 or not c2,c4,v2 are_collinear or not c2,c4,v3 are_collinear or v2,v3,c2 are_collinear ) ) & c2,c4,c6 are_collinear & c2,c4,c1 are_collinear )
(
c6,
c1,
c1 are_collinear &
c6,
c1,
c5 are_collinear )
by COLLSP:2, A5, HESSENBE:1;
hence
not
c6,
c1,
c2 are_collinear
by A2, COLLSP:3, A3;
( ( for v3, v2 being Element of PCPP holds
( c4 = c2 or not c2,c4,v2 are_collinear or not c2,c4,v3 are_collinear or v2,v3,c2 are_collinear ) ) & c2,c4,c6 are_collinear & c2,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 )
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; hence
for
v3,
v2 being
Element of
PCPP holds
(
c4 = c2 or not
c2,
c4,
v2 are_collinear or not
c2,
c4,
v3 are_collinear or
v2,
v3,
c2 are_collinear )
;
( c2,c4,c6 are_collinear & c2,c4,c1 are_collinear )thus
c2,
c4,
c6 are_collinear
by A6, A7, HESSENBE:1;
c2,c4,c1 are_collinear thus
c2,
c4,
c1 are_collinear
by A4, COLLSP:8;
verum end;
hence
contradiction
by A1; verum