let PCPP be CollProjectiveSpace; for c1, c2, c5, c6, c7 being Element of PCPP st not c1,c2,c5 are_collinear & c1,c5,c6 are_collinear & c1,c5,c7 are_collinear holds
c5,c6,c7 are_collinear
let c1, c2, c5, c6, c7 be Element of PCPP; ( not c1,c2,c5 are_collinear & c1,c5,c6 are_collinear & c1,c5,c7 are_collinear implies c5,c6,c7 are_collinear )
assume that
A1:
not c1,c2,c5 are_collinear
and
A2:
c1,c5,c6 are_collinear
and
A3:
c1,c5,c7 are_collinear
and
A4:
not c5,c6,c7 are_collinear
; contradiction
now ( ( for v100, v2 being Element of PCPP holds v2,v100,v100 are_collinear ) & ( for v0 being Element of PCPP holds
( not c1,c5,v0 are_collinear or v0,c6,c7 are_collinear ) ) )thus
for
v100,
v2 being
Element of
PCPP holds
v2,
v100,
v100 are_collinear
by COLLSP:2;
for v0 being Element of PCPP holds
( not c1,c5,v0 are_collinear or v0,c6,c7 are_collinear )
( not
c5 = c1 or
c1,
c2,
c5 are_collinear )
by COLLSP:2;
hence
for
v0 being
Element of
PCPP holds
( not
c1,
c5,
v0 are_collinear or
v0,
c6,
c7 are_collinear )
by COLLSP:3, A1, A2, A3;
verum end;
hence
contradiction
by A4; verum